\documentclass[xcolor=table,11pt,a4paper]{article}
\usepackage[table,xcdraw]{xcolor}
\usepackage[spanish]{babel}
\usepackage[utf8]{inputenc}
\usepackage[font=footnotesize,labelfont=bf]{caption}
\usepackage{algpseudocode}
\usepackage{algorithm}
\usepackage{enumerate}
\usepackage{comment}
\usepackage{verbatim}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath, amssymb}
\usepackage{latexsym}
\usepackage[toc,page]{appendix}
\usepackage{qtree}
\usepackage{tikz}
\usepackage{tikz-qtree}
\usepackage{cancel}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{textcomp}
\usepackage[T1]{fontenc}
\usepackage{multicol}
\usepackage{babelbib}
\usepackage{url}
\definecolor{codebg}{HTML}{EEEEEE}
\definecolor{codeframe}{HTML}{CCCCCC}
\lstset{
	backgroundcolor=\color{codebg},
	frame=single,
	framesep=10pt,
	framerule = 0pt,
	rulecolor=\color{codeframe},
	upquote=true,
	basicstyle=\ttfamily\small,
	captionpos=b
}

\renewcommand{\lstlistingname}{Fragmento}

\renewenvironment{abstract}
 {\small
  \begin{center}
  \bfseries \abstractname\vspace{-.5em}\vspace{0pt}
  \end{center}
  \list{}{%
    \setlength{\leftmargin}{30mm}
    \setlength{\rightmargin}{\leftmargin}
  }%
  \item\relax}
 {\endlist}

\include{caratula/caratula}

\begin{document}


%---------------------  Título ---------------------%
\titleGP
\clearpage

%--------------------  Abstract --------------------%
\begin{abstract}
El algoritmo de encriptación de información AES (Advanced Encryption Standard) es un estándar internacional ampliamente utilizado tanto por gobiernos como comercialmente; por lo tanto resulta de importancia crítica garantizar el correcto comportamiento de sus  distintas implementaciones. Existe una versión simplificada del algoritmo, llamada Mini-AES, que fue creada con fines académicos pero sin perder la esencia de su funcionamiento y sus propiedades criptográficas. En este trabajo se define un lenguaje de programación imperativa, se implementa Mini-AES sobre el mismo y se demuestra formalmente que su comportamiento es el deseado, esto es, que los procedimientos de encriptar y desencriptar son inversos. El lenguaje de programación en el cual se define el algoritmo Mini-AES se formaliza en el asistente de pruebas Coq, que es utilizado también para desarrollar pruebas sobre el comportamiento de dicho algoritmo, utilizando lógica de Hoare.
Se presenta entonces una especificación formal del algoritmo Mini-AES junto con su correspondiente implementación funcionalmente correcta.
\end{abstract}

\clearpage

%---------------  Tabla de contenidos --------------%
\tableofcontents

\clearpage

%------------------- Introducción ------------------%
\section{Introducción}
Dada la masificación actual de sistemas informáticos de toda categoría, ya sean estos empresariales, gubernamentales, relacionados a la salud, redes sociales, almacenamiento en la nube, o de esparcimiento personal, y la importancia de los mismos en cuanto a la información que contienen, resulta crítico que su funcionamiento sea seguro y confiable. La gran mayoría de estos sistemas manipulan de alguna forma información que puede llegar a ser utilizada con fines que resulten perjudiciales a quienes los emplean, o simplemente con un fin distinto al original. Para poder garantizar su uso confiable, dichos sistemas deben muchas veces proveer garantías de privacidad de la información o de autenticidad de origen \cite{Stallings}. En computación ello implica el manejo de primitivas criptográficas. La criptografía es un área de estudio amplia que provee herramientas sobre las cuales se puede basar la computación para garantizar las necesidades mencionadas \cite{cryptography}. Pero existe una distancia entre la teoría en criptografía y su aplicación práctica en la computación, ya sea debido a limitaciones físicas que pueden ser de espacio o tiempo, o simplemente debido a errores humanos al aplicar la teoría.

La motivación de este trabajo es acortar la distancia entre la teoría y su aplicación práctica para poder contar con sistemas informáticos que sean seguros. Para ello es necesario validar los lenguajes de programación y los algoritmos escritos en ellos, utilizando herramientas teóricas como modelos y demostraciones formales.

\subsection{Objetivos del trabajo}
Los objetivos de este trabajo son diseñar un lenguaje de tipo imperativo e implementar sobre éste los algoritmos AES (Advanced Encryption Standard) \cite{Standards2001} y Mini-AES \cite{miniAES} para que sirvan como implementaciones de referencia. Además para Mini-AES se pretende probar formalmente que la implementación de referencia es correcta funcionalmente. Entendemos por corrección funcional al comportamiento del algoritmo desde el punto de vista de la relación entre su entrada y su salida. Se espera que los procedimientos de encriptar y desencriptar sean inversos, es decir que al encriptar una entrada y desencriptar el resultado se obtenga una salida idéntica a la entrada original.

\subsection{Trabajos relacionados}
A la fecha de la publicación de este trabajo no encontramos otros trabajos que se encuentren vinculados a esta temática y que sigan el mismo enfoque. Por lo tanto consideramos al presente un aporte en el área, a partir del cual se puede continuar en la línea de investigación.
A continuación mencionamos algunos proyectos cuyos objetivos se encuentran relacionados de alguna forma con el presente.

\subsubsection*{CompCert}
\textit{CompCert} \cite{CompCert} es un trabajo muy completo en el que se verifica la corrección de compiladores de algunos lenguajes de programación. Su principal resultado es \textit{CompCert C}, un compilador de ISO C90 / ANSI C que genera código para las arquitecturas PowerPC, ARM y x86.
La importancia de \textit{CompCert} radica en brindar un compilador que se encuentra verificado mediante pruebas matemáticas que garantizan la correspondencia entre la semántica del código fuente y el código generado.
El compilador completo se encuentra especificado, programado y verificado en Coq, y es liderado por Xavier Leroy, quien comenzó el proyecto en 2005. Actualmente se encuentra en desarrollo y se cuenta con la verificación formal del 90\% de los algoritmos del compilador.

El enfoque de este proyecto es obtener un compilador certificado. Al utilizar un compilador certificado se garantiza que el código generado es una traducción sin errores desde el lenguaje original hacia el objetivo, pero no se puede probar que el algoritmo en el lenguaje original se encuentre correctamente implementado.

\subsubsection*{Ynot}
\textit{Ynot} \cite{Ynot} es una librería desarrollada en Coq \cite{Coq:manual} que permite escribir programas imperativos y verificarlos. Esta librería implementa una extensión de la lógica de Hoare, denominada lógica de separación y cuenta con tácticas automatizadas que permiten probar fórmulas de este estilo.
El proyecto se encuentra soportado por la National Science Foundation y Microsoft Research.

\subsubsection*{CertiCrypt}
\textit{CertiCrypt} \cite{CertiCrypt} es una serie de herramientas para la construcción y verificación de algoritmos criptográficos. Soporta patrones comunes para razonar en criptografía, y ha sido utilizada para probar la seguridad de algunas construcciones, incluyendo esquemas de firma digital y funciones de hash.
Su principal resultado es un framework verificado formalmente sobre Coq. Se basa en un lenguaje de programación extensible, probabilista e imperativo.
Este proyecto fue fundado por el INRIA-Microsoft Research Joint Centre y el proyecto del Agence Nationale Recherche \textit{SCALP} entre otros.

\subsection{Estructura del documento}
En el resto de esta sección se muestra un breve marco conceptual de criptografía en general, se introducen los algoritmos AES y Mini-AES. También se explican algunos conceptos del asistente de pruebas Coq \cite{Coq:manual}, así como el modelado de lenguajes sobre el mismo.

En la sección \ref{sec:lenguaje} se presenta el lenguaje desarrollado para el trabajo, donde se detalla su sintaxis y semántica, además del módulo de matrices que fue necesario para poder completar la implementación. La sección~\ref{sec:aes} explica el funcionamiento detallado del algoritmo AES y Mini-AES, para el último se muestra su implementación en el lenguaje explicado anteriormente. Luego en la sección \ref{sec:hoare} se introducen los conceptos básicos de la lógica de Hoare así como su utilización en nuestro caso de estudio. En la sección \ref{sec:correccion} se explica la verificación del algoritmo. Finalmente en la sección \ref{sec:conclusiones} se presentan las conclusiones y el trabajo a futuro. A continuación de las referencias bibliográficas se incluyen los anexos \ref{anexo:lenguaje}, \ref{anexo:aes_impl} y \ref{anexo:prueba} que contienen la especificación completa del lenguaje, la implementación completa de Mini-AES y la prueba completa de corrección, respectivamente.

\subsection{Marco conceptual}

\subsubsection{Criptografía simétrica}
Se define texto \textit{plano} como un mensaje o información en su forma original y texto \textit{cifrado} o \textit{encriptado} como la codificación del texto plano en una cierta forma que aparente ser un flujo de información aleatoria o sin sentido, pero que podrá ser procesada solamente por entidades autorizadas para recuperar el texto plano. También se define \textit{encriptación} o \textit{codificación} como el proceso de transformar texto plano en texto cifrado y \textit{desencriptación} o \textit{decodificación} como el proceso de recuperar el texto plano a partir del cifrado.
Los esquemas utilizados para encriptar, que se denominan \textit{sistemas criptográficos}, constituyen un área de estudio llamada \textit{criptografía} y las técnicas para desencriptar un texto cifrado sin conocimiento de los detalles de encriptación forman el área de \textit{criptoanálisis}. Las áreas de criptografía y criptoanálisis en conjunto son llamadas \textit{criptología}.

Durante el proceso de encriptación y desencriptación, los algoritmos criptográficos utilizan un parámetro de entrada especial denominado \textit{clave} el cual determina la salida específica del algoritmo, haciendo que el mismo texto al ser encriptado con dos claves distintas produzca salidas distintas. Se puede ver entonces al proceso de encriptación como una función que recibe de entrada un texto plano y una clave y produce como salida un texto cifrado. En el sentido opuesto, la desencriptación es una función que realiza el procedimiento inverso y, dado un texto cifrado junto con una clave, devuelve el texto plano original. Resumiendo, dados un texto plano $X$ y las claves $K_e$ y $K_d$, las funciones de encriptación y desencriptación, denominadas $e$ y $d$ respectivamente, deben cumplir:
\begin{equation} \label{theo:inverse}
e(X,K_e) = Y\ \rightarrow\ d(Y,K_d) = X
\end{equation}
Actualmente existen dos modelos mediante los cuales se categorizan los algoritmos de encriptación: por un lado los algoritmos \textit{simétricos} o \textit{de clave privada} y por otro los \textit{asimétricos} o \textit{de clave pública}. La principal diferencia entre ambos modelos radica en que para los algoritmos simétricos se cumple $K_e = K_d$, es decir que se utiliza la misma clave tanto para el procedimiento de encriptar como el de desencriptar, mientras que los algoritmos de clave pública utilizan dos claves distintas. La mayor utilidad práctica de contar con dos claves diferentes es poder publicar la clave mediante la cual se encripta ---clave pública, de forma que cualquiera pueda encriptar y enviar texto codificado pero solamente el receptor de dicho texto, haciendo uso de la otra clave que solamente él conoce ---clave privada, pueda desencriptar e interpretar el mensaje original. Si bien los algoritmos de clave pública tienen más utilidades que las aquí mencionadas, nuestro objetivo es trabajar con AES que es simétrico y por lo tanto no profundizaremos en dicho tema.

Volviendo a la ecuación~\ref{theo:inverse}, se define $X = [X_1, X_2, ..., X_N]$ donde $X_i$ es una letra de un alfabeto finito, que en nuestro contexto es el alfabeto binario $\{0,1\}$. De la misma forma, $K = [K_1, K_2, ..., K_L]$ y $Y = [Y_1, Y_2, ..., Y_M]$, notar que a la clave al ser única es denominada sin subíndice, simplemente $K$. Con el mensaje $X$ y la clave $K$ se puede utilizar la función $e$ para generar el texto cifrado $Y = e(X,K)$ y luego quien posea la clave ---que se espera sea el destinatario del mensaje, puede utilizar la función $d$ para acceder a $X = d(Y,K)$. Ahora bien, un atacante observando $Y$ puede intentar acceder a $X$ o $K$ o ambos. Si está interesado en recuperar solamente el actual mensaje entonces intentará recuperar $X$ generando un texto plano estimado $\hat{X}$. Sin embargo, por lo general el atacante está interesado en leer también futuros mensajes y para ello debe recuperar $K$ generando una clave estimada $\hat{K}$.

Los algoritmos criptográficos más utilizados basan su seguridad en la clave y no en el algoritmo en sí mismo. Esto quiere decir que conocer el algoritmo además del texto cifrado no debe ser de ninguna ayuda para descifrarlo. Para generar $\hat{K}$ existen dos enfoques: \textbf{criptoanálisis} y \textbf{fuerza bruta}. El criptoanálisis busca aproximarse a la clave o a un texto plano basándose en las características del comportamiento del algoritmo, analizando posibles debilidades en su funcionamiento que puedan ser explotadas por un atacante. Por otro lado la fuerza bruta consiste en intentar con cada posible combinación de clave hasta encontrar un texto plano adecuado, notar que en promedio se puede dar con la clave al probar con la mitad de todas las combinaciones posibles.

\subsubsection{Propiedades de un algoritmo seguro}
Para que un algoritmo simétrico sea considerado seguro, un atacante no debe ser capaz de decodificar el texto cifrado o descubrir la clave, aún teniendo una cantidad de textos planos con sus correspondientes textos cifrados. En cuanto al manejo de la clave, tanto quien encripta como quien desencripta el texto deben haber obtenido la clave de forma segura y así deben mantenerla. Si un atacante descubre la clave y conoce el algoritmo, toda comunicación podrá ser leída por el mismo.

Las razones por las cuales AES realiza las operaciones que estudiaremos, se basan fuertemente en conceptos de criptografía. Presentamos aquí brevemente las nociones mínimas necesarias para comprender dichas operaciones ya que profundizar en dichos temas escapa al alcance de este trabajo pero se puede estudiar en mayor profundidad estos temas en \cite{Stallings}.

\paragraph{Confusión}
Esta propiedad implica que no debe existir una relación sencilla entre la clave y el texto cifrado, por lo tanto cada caracter del texto cifrado debe depender de la mayoría de los bits de la clave. Esto hace que sea difícil descubrir la clave, aún teniendo acceso a un conjunto grande de parejas de texto plano junto con su versión cifrada, todas utilizando la misma clave ---este tipo de ataque se categoriza como \textit{known-plaintext}. Por ello es importante que en la práctica cada bit del texto cifrado dependa de todos los bits de la clave y en diferentes maneras de cada uno.

\paragraph{Difusión} Por otro lado, la relación entre el texto plano y el texto cifrado debe ser también compleja. Más precisamente, dado un texto plano cualquiera de entrada y su correspondiente texto cifrado de salida, al cambiar un bit en la entrada la probabilidad de cambiar para cada bit de la salida es 0.5, o sea que al menos la mitad de los bits deben cambiar al tomar el promedio de todos. Esta propiedad es importante para evitar los ataques categorizados como \textit{chosen-plaintext} en los cuales el atacante tiene acceso a elegir textos planos arbitrarios para ser encriptados y obtener su cifrado.

\paragraph{No linealidad}
Siendo vista como una función, la encriptación de un bloque de texto plano no debe poder distinguirse de una permutación aleatoria de los bits. En caso de que esto no ocurriera, existe una técnica denominada \textit{criptoanálisis lineal} que es capaz de encontrar transformaciones \textit{afines} y mediante ciertos mecanismos descubrir bits de la clave. Junto con el \textit{criptoanálisis diferencial} estas son las técnicas más utilizadas contra los algoritmos de cifrado por bloques.\\

Las dos primeras propiedades mencionadas ---confusión y difusión--- se logran por lo general utilizando lo que se llama una \textit{red de sustitución-permutación}, y AES es un ejemplo de ello. Básicamente, este tipo de algoritmos consiste en una serie de operaciones matemáticas donde cada una de ellas se aplica a los bits de entrada y su salida es la entrada para la siguiente operación. Dichas operaciones son, como lo dice su nombre, sustituciones y permutaciones de los bits de entrada, veremos en AES cómo estas operaciones se llevan a la práctica.

\subsubsection{El estándar AES}
El denominado AES es una especificación para la codificación y decodificación de datos digitales. Su historia comienza en el año 1997 cuando el NIST (National Institute of Standards and Technology) decide realizar una convocatoria pública para recibir propuestas sobre un algoritmo de encriptación simétrico que fuera un estándar no clasificado y divulgado públicamente. Este algoritmo debía ser capaz de proteger la información del gobierno de los Estados Unidos para el siguiente siglo, incluyendo información de sensibilidad nivel \textit{top secret}.

Su predecesor, el Data Encryption Standard (abreviado DES), fue seleccionado luego de una convocatoria de características similares realizada en 1973. En 1974, la multinacional IBM propuso un algoritmo diseñado por Horst Feistel, que sería seleccionado como estándar en 1976 y publicado oficialmente como Federal Information Processing Standard (FIPS) en 1977 por el NIST, que en ese entonces se llamaba NBS (National Bureau of Standards). Al ser elegido como un estándar por el gobierno, DES ganó adopción internacionalmente en muchas otras áreas y también fue estudiado y criticado en ámbitos acádemicos. A pesar de haber generado ciertas controversias debido a ciertos elementos de diseño que eran clasificados o a su reducido tamaño de clave de 56 bits, este algoritmo se consolidó como estándar internacional de encriptación simétrica durante los siguientes veinte años; su especificación aún se conserva en los archivos del NIST \cite{des}.

Para fines de la década de los 90 el tamaño de clave de 56 bits ya resultaba vulnerable a ataques de fuerza bruta, además de que DES fue pensado para correr en hardware y resulta poco eficiente a la hora de ser implementado en software. Por ello fue realizada la convocatoria por el NIST en 1997 y el proceso de selección se realizó en tres etapas que se pueden relacionar con las tres conferencias denominadas AES1, AES2 y AES3. Desde la convocatoria realizada en setiembre de 1977 hasta la primera conferencia, fueron presentados en total quince algoritmos: CAST-256, CRYPTON, DEAL, DFC, E2, FROG, HPC, LOKI97, MAGENTA, MARS, RC6, Rijndael, SAFER+, Serpent y Twofish. En las primeras dos conferencias, realizadas en agosto de 1998 y marzo de 1999 respectivamente, se discutieron las ventajas y desventajas de cada candidato en cuanto a seguridad y performance, se descartaron algunos de ellos y se llegó a los cinco denominados \textit{finalistas}: Rijndael, Serpent, Twofish, RC6 y MARS. En la conferencia AES2 se realizó una votación en la cual Rijndael obtuvo 86 votos positivos y 10 negativos, seguido por Serpent el cual obtuvo 59 positivos y 7 negativos. En la última conferencia, AES3 realizada en abril del año 2000, un representante por el equipo de cada candidato realizó una presentación sobre las razones por las cuales consideraba mejor su algoritmo. Luego de un intenso debate, en octubre del mismo año el NIST anunció que había seleccionado a Rijndael y luego de realizar un borrador solicitando comentarios, en noviembre de 2001 se aprueba Rijndael como el FIPS 197 \cite{Standards2001}.

Rijndael fue diseñado por los belgas Joan Daemen y Vincent Rijmen ---su nombre es una conjunción de los apellidos--- y su propuesta puede encontrarse en \cite{rijndael}. Debido a su riguroso proceso de selección y al ser el sucesor de un estándar que llegó a durar veinte años en la industria, se espera que AES pueda ser utilizado quizás por otros tantos años más.

El algoritmo se categoriza como algoritmo simétrico y por bloques; simétrico por utilizar una misma clave tanto para el proceso de encriptar como para el de desencriptar y por bloques debido a que opera sobre grupos de bits de largo fijo, aplicando una transformación invariante sobre cada uno de dichos bloques. Las claves de AES pueden tener un tamaño de 128, 192 o 256 bits y el tamaño del bloque es 128 bits. La estructura del algoritmo es una red de sustitución-permutación ya que consiste en realizar un número de \textit{rondas} determinado, aplicando una serie de operaciones matemáticas a cada bloque del texto en cada una de las mismas.

Hasta el día de hoy no existen ataques computacionalmente posibles contra AES y su complejidad es de 2\textsuperscript{126.1}, 2\textsuperscript{189.7} y 2\textsuperscript{254.4} para claves de 128, 192 y 256 bits respectivamente, utilizando el denominado método biclique, que solamente es mejor que aplicar fuerza bruta en un factor de cuatro.

Otras de sus cualidades son su performance en cómputo y memoria, así como su simplicidad de implementar tanto en software como en hardware. Hoy existen procesadores relativamente económicos, de uso personal, que implementan una extensión de la arquitectura x86 llamada AES-NI (AES New Instructions) con instrucciones para ejecutar una ronda completa de encriptación o expandir la clave por ejemplo. Utilizando estas primitivas, existen librerías que pueden llegar a procesar texto a una velocidad de 700 MB/s por thread.

Debido a las cualidades mencionadas es uno de los algoritmos más populares, siendo utilizado por herramientas de compresión, servidores y navegadores web, protocolos de acceso remoto, sistemas operativos y protocolos de comunicación en redes de área local, entre otros ejemplos. Es por esto que AES es considerado como un algoritmo de seguridad crítico.

\subsubsection{Mini-AES}
En el año 2002, casi inmediatamente luego de que fuera publicado oficialmente AES, el criptólogo de la \textit{Multimedia University} e investigador del instituto \textit{Swinburne Sarawak Institute of Technology}, instituciones de Malasia  Raphael Chung-wei Phan , publicó un artículo denominado \textit{Mini Advanced Encryption Standard (Mini-AES): A Testbed for Cryptanalysis Students} \cite{miniAES}. Allí se presenta una versión reducida del AES, simplificando los parámetros que se manejan en el mismo pero, como es aclarado en el mismo artículo, sin perder la estructura original. Basándose en Mini-AES es posible estudiar las propiedades de AES, de manera tal de concentrarse en las partes más relevantes para este trabajo.

\subsubsection{Lenguajes para criptografía}
\label{subsec:lenguajes_criptografia}
Actualmente hay disponibles varias implementaciones de AES, se pueden encontrar librerías para los lenguajes más populares como lo son Java, C/C++, C\#, Objective-c, PHP, Python, Ruby, Perl, Javascript, Haskell u OCaml. A pesar de poder encontrarse en cualquier tipo de lenguaje, las más utilizadas son las implementaciones en C o en su defecto en lenguajes basados en este como lo son C++, Java y C\#. Por ejemplo, en C se pueden destacar las librerías PolarSSL \cite{PolarSSL}, Libgcrypt \cite{Libgcrypt} y OpenSSL \cite{OpenSSL} de las cuales las últimas dos se encuentran validadas por el NIST como correctamente implementadas ---ver \cite{nist_validation}. En cuanto a C++ se cuenta con Crypto++ \cite{Crypto++} y Botan\cite{Botan} de particular relevancia y la primera se encuentra también validada por el NIST. Por parte de la plataforma Java se puede nombrar la Java Cryptography Extension (JCE) que es un framework el cual debe ser proveído por la versión utilizada pero por ejemplo Oracle provee su propia implementación ver \cite{Oracle_Crypto} y también Bouncy Castle \cite{Bouncy_Castle} que es muy utilizada en la industria.

Estos lenguajes comparten como característica principal ser imperativos y estáticamente tipados. Poseen tipos de datos básicos para representar booleanos y enteros y realizar operaciones sobre estos ---tanto operaciones aritméticas como bit a bit--- y tipos más complejos como arreglos y a partir de ellos matrices. Además brindan estructuras de control como \textit{if}, \textit{for} y \textit{while}.

\subsubsection{El asistente de pruebas Coq}
Se eligió \textit{Coq} \cite{Coq:manual} como herramienta principal para el trabajo. Este es un asistente de pruebas, que sirve para expresar definiciones matemáticas así como escribir pruebas sobre las mismas y verificar dichas pruebas automáticamente. Además de esto permite escribir programas y ejecutarlos, especificar propiedades sobre los mismos y hasta extraer código ejecutable de la prueba realizada sobre la especificación.

\textit{Coq} implementa un lenguaje llamado \textit{Gallina}, basado en la teoría conocida como \textit{Cálculo inductivo de contrucciones} (CiC), la cual a su vez es una extensión del \textit{Cálculo de construcciones} \cite{cic}. Esta última fue creada por Thierry Coquand, quien también comenzó el desarrollo de Coq en el año 1984. En el CiC, los programas, sus propiedades y sus pruebas, son formalizados bajo el mismo lenguaje y por lo tanto todos los juicios lógicos terminan reduciéndose a juicios de tipado.

\subsubsection{Modelado de lenguajes en Coq}
Coq provee un lenguaje formal mediante el cual se puede modelar la sintaxis y semántica del lenguaje objetivo. Utilizando definiciones inductivas en Coq se puede modelar la sintaxis de un lenguaje de forma clara y concisa. Por ejemplo la siguiente definición es válida en Coq y muestra una posible definición de expresión aritmética con operadores de suma, resta y multiplicación:
\begin{lstlisting}[caption=Ejemplo de definición de expresión sintáctica., mathescape]
Aexp :=
  arith_num   : nat  $\rightarrow$ Aexp
  arith_plus  : Aexp $\rightarrow$ Aexp $\rightarrow$ Aexp
  arith_minus : Aexp $\rightarrow$ Aexp $\rightarrow$ Aexp
  arith_mult  : Aexp $\rightarrow$ Aexp $\rightarrow$ Aexp
\end{lstlisting}
Luego es posible escribir una expresión de la siguiente forma, que representa la noción más común de $3 * (2 + 4)$:
\begin{lstlisting}
arith_mult (arith_num 3) (arith_plus (arith_num 2) (arith_num 4))
\end{lstlisting}

\subsection{Notación utilizada}
Debido a que el trabajo está fuertemente basado en Coq, muchas de las notaciones son tomadas directamente del lenguaje Gallina.

\subsubsection*{Expresiones lógicas}
\label{subsubsec:expresiones}
Para las expresiones lógicas son utilizados los operadores estándar: $\wedge$ (conjunción o \textit{and}), $\lor$ (disjunción u \textit{or}), $\lnot$ (negación o \textit{not}), $\rightarrow$ (implicación), $\forall$ (cuantificación universal) y $\exists$ (cuantificación existencial). Estas expresiones son escritas en cursiva y centradas como se muestra en el siguiente ejemplo:
\[
\forall\ (i\ j:\ \mathbb{N}),\ \exists\ (m:\ \mathbb{N}),\ m > i + j\ \rightarrow\ m > i\ \land\ m > j
\]

\subsubsection*{Código fuente}
Por otro lado, las citas a código fuente como nombres de variables o tipos son escritas en letra estilo Courier, por ejemplo \texttt{int i ::= 0;} cuando se encuentra dentro de un párrafo. Al insertar fragmentos de código se utiliza un recuadro como el siguiente:
\begin{lstlisting}[caption=Ejemplo de fragmento de código.]
byte a ::= matrix[0][0];
matrix[0][1] ::= a;
\end{lstlisting}

\subsubsection*{Tipos inductivos}
Se ven a lo largo de este documento varios ejemplos de definiciones mediante tipos inductivos, esto no es casual, ya que este trabajo se basa fuertemente en el CiC. La sintaxis utilizada es simplemente: el nombre del tipo seguido de \texttt{:=} y la lista de constructores, uno por línea, como en el siguiente ejemplo:
\begin{lstlisting}[caption=Ejemplo de definición de tipo inductivo., mathescape]
Natural :=
  zero : Natural
  suc  : Natural $\rightarrow$ Natural
\end{lstlisting}

\subsubsection*{Tipos y funciones}
Para definir el tipo de un conjunto de símbolos se colocan sus nombres separados por espacios y dos puntos para introducir el tipo, por ejemplo \texttt{i j: Integer}. En el caso de requerir más de un tipo, se separan utilizando paréntesis como \texttt{(m n: Natural)(i j: Integer)}.
Las funciones son definidas mediante su nombre, seguido de todos sus parámetros con sus correspondientes tipos, dos puntos para introducir (opcionalmente) el tipo de retorno y luego \texttt{:=} para separar de la definición. El siguiente es un ejemplo de función:
\begin{lstlisting}[caption=Ejemplo de definición de función.]
sum (m n: Natural): Byte := m + n
\end{lstlisting}

Al aplicar una función, se utilizan espacios y asociación a la izquierda como se hace en Gallina o Haskell. Por ejemplo la función \texttt{sum} recién definida se aplica de la siguiente forma: \texttt{sum (sum 1 1) 5}.

\subsection{Código fuente}
\label{subsec:codigo}
Todo el código fuente generado como parte de este trabajo se encuentra disponible en \cite{Codigo}. Allí se puede encontrar un archivo de texto llamado \textit{README} que contiene una breve explicación sobre cómo compilar los módulos y ejecutar las pruebas.

%------------------- Introducción ------------------%

\clearpage

%------------------- Lenguaje ------------------%
\section{Lenguaje}
\label{sec:lenguaje}
Las implementaciones mencionadas en la sección \ref{subsec:lenguajes_criptografia} contienen código que puede resultar sumamente complejo de utilizar para realizar demostraciones formales como las que se plantean en este trabajo. Por otro lado, elegimos el algoritmo Mini-AES como objetivo para nuestras pruebas, ya que justamente simplifica la comprensión de AES. Aprovechamos entonces la oportunidad de tener que implementar Mini-AES para hacerlo sobre un lenguaje de programación definido en Coq. Esto nos brinda una mayor flexibilidad al realizar las pruebas y nos permite además tener una versión del algoritmo que puede servir como referencia para implementaciones en otros lenguajes.

Dado que precisamos un lenguaje para criptografía y en particular poder implementar los algoritmos AES y Mini-AES ---presentados en \cite{rijndael_libro} y \cite{miniAES}--- es necesario analizar las principales características con las que cuentan los lenguajes utilizados para dicho propósito. Como ya fue visto en la sección~\ref{subsec:lenguajes_criptografia}, estos siguen el paradigma imperativo y por lo tanto debemos modelar primitivas fundamentales como lo son la asignación de valores a variables en memoria y la ejecución de secuencias de instrucciones.

Luego de estudiar el funcionamiento de los algoritmos ---detallados en la sección \ref{sec:aes}--- contamos con una visión más precisa sobre las funcionalidades que debe proveer nuestro lenguaje. Dichas funcionalidades abarcan básicamente manipulación de bytes: asignación en memoria, suma exclusiva, búsqueda en una posición de una matriz, asignación a una posición de matriz y estructuras de control y repetición.

Pero también resulta interesante para el trabajo que el lenguaje sea completo, para que se pueda continuar trabajando sobre el mismo. Por eso lo desarrollamos basándonos en \cite{SF} y extendiéndolo para que cuente con las siguientes características: tipos de datos entero, byte, booleano y matrices; así como manejo de variables, sentencias condicionales y loops. Contamos entonces con un modelo de lenguaje imperativo sobre el cual se puede implementar no solamente los algoritmos AES y Mini-AES, sino que teóricamente cualquier algoritmo ---debido a que es Turing-completo \cite{turing}--- y que en la prácitca resulta especialmente útil para algoritmos criptográficos.

Para que la sintaxis del lenguaje pueda ser reutilizada, decidimos implementarla de forma modular, definiendo en un módulo la sintaxis y manteniendo tanto a los tipos de datos como a sus operaciones de manera abstracta. Así, uno puede utilizar diferentes implementaciones de enteros, bytes, suma o resta por nombrar algunos ejemplos. Esto se puede lograr en Coq definiendo un módulo como \texttt{Module Type}, dentro del cual declaramos los tipos de datos y sus operaciones como parámetros. Luego hacemos a la sintaxis y semántica del lenguaje dependientes del módulo de tipos y éstas pueden utilizar los tipos de datos sin tener que conocer los detalles de su implementación.

A lo largo de la definición del lenguaje se puede ver que se realizan referencias a estos tipos de datos y sus operaciones. Los nombres de los tipos son introducidos en la sección~\ref{subsec:tipos} y los nombres de las operaciones se distinguen sencillamente, siendo el nombre del tipo y operación separados por un guión bajo como por ejemplo \texttt{int\_plus}.
En caso de modificar la implementación de alguno de ellos, no es necesario en absoluto modificar la definición del lenguaje.

En este trabajo utilizamos las implementaciones de la librería estándar de Coq donde nos es posible, la única excepción son las matrices, que son explicadas más adelante.

A continuación presentamos la sintaxis de nuestro lenguaje y luego la semántica.

\subsection{Sintaxis}

\subsubsection{Estructura de un programa}
\label{subsec:estructura_programa}
Veamos primero cómo se compone a grandes rasgos un programa en este modelo. Básicamente, un programa consiste de un conjunto de variables globales y definiciones de procedimientos que pueden tomar parámetros. Las variables no contienen información de tipo, por lo cual al ser declaradas no se les asigna ningún tipo pero debe ser especificado a la hora de leer o escribir un valor. Los procedimientos se definen mediante su nombre, los parámetros entre paréntesis y a continuación el cuerpo del mismo.

Todas estas definiciones ---identificadores y procedimientos--- se introducen luego de su nombre mediante el símbolo \texttt{:=} y se separan por medio de un punto. Esto no es arbitrario ya que se trata de definiciones válidas en Coq, en el código fuente se puede observar que las mismas deben ser precedidas por la palabra clave \texttt{Definition}, que omitimos en este documento en favor de una mayor claridad.
\begin{lstlisting}[caption=Estructura de un programa., label={lst:estructura}]
two := id 1.

double(num: Id) :=
  int two ::= 2;
  int num ::= num * two;
.

plus_three(num: Id) :=
  int num ::= num + 3;
.

double_plus_three(num: Id) :=
  double num;
  plus_three num;
.
\end{lstlisting}
En el fragmento~\ref{lst:estructura} se puede notar que siempre utilizamos parámetros para modificarlos, esto se debe a que no fue implementado el tipo de procedimientos con \textit{retorno} de un nuevo valor, ya que esto agregaba mucha complejidad extra y escapaba del alcance de este proyecto. Por lo tanto se debe modificar una variable para realizar un efecto externamente visible.

También se puede observar que utilizamos símbolos característicos para las operaciones, como por ejemplo \texttt{*} para la multiplicación y \texttt{+} para la suma. Esto es posible realizarlo en Coq utilizando \texttt{Notation}s y fue utilizado en este trabajo para permitir escribir código más conciso; en cada subsección del anexo \ref{subsec:apendice_sintaxis}  mostramos una tabla con los símbolos correspondientes a las operaciones.

\subsubsection{Tipos de datos} \label{subsec:tipos}
Es imprescindible contar con números enteros para ser utilizados en contadores y loops entre otras operaciones fundamentales, así como valores binarios para utilizar por ejemplo en sentencias condicionales, es por ello que el lenguaje cuenta con los tipos \texttt{Integer} y \texttt{Bool}. Este lenguaje cuenta también con los tipos \texttt{Byte} y \texttt{Matrix}, que tienen claramente el objetivo de ser utilizados para AES y Mini-AES y serán de hecho los más utilizados en este trabajo. El tipo \texttt{Matrix} nos permite representar matrices de bytes aunque puede ser fácilmente extendido a matrices de otros tipos.

\subsubsection{Identificadores}
\label{subsec:identificadores}
La forma más sencilla de representar las variables es viendo a la memoria como un arreglo de posiciones, donde un valor puede ser asignado en cualquiera de ellas. Podemos asignarle entonces a una variable un identificador, que no es más que un número natural indicando la posición ocupada en memoria; como consecuencia, si dos variables se encuentran identificadas por el mismo identificador entonces al escribir cualquiera de ellas estaremos escribiendo la misma posición en memoria y sobrescribiendo mutuamente los valores.

Para los identificadores creamos el tipo \texttt{Id}, este se trata simplemente de un tipo inductivo con un único constructor, que toma un número natural como parámetro:
\begin{lstlisting}[mathescape, caption=El tipo de los identificadores]
Id :=
  id : nat $\rightarrow$ Id
\end{lstlisting}
Por lo tanto \texttt{id 1} es una expresión de tipo \texttt{Id}, y al asignarle un nombre mediante una definición ---como \texttt{two} en la primera línea del fragmento~\ref{lst:estructura}--- decimos que se trata de una variable.

\subsubsection{Expresiones}
Las expresiones son las que van a permitir al programador representar valores correspondientes a los tipos de datos disponibles. Por ejemplo, un valor correspondiente a los números enteros, que en nuestro lenguaje es el tipo de datos \texttt{Integer}, puede ser un número literal como \texttt{12} o también puede ser una suma entre números enteros como \texttt{12 + 1}. Pero también se pueden representar valores de otros tipos, como por ejemplo \texttt{3 <\ 4}, el cual es de tipo \texttt{Bool} y es el resultado de la comparación entre ambos números enteros; o un valor de tipo \texttt{Byte} que es sea el resultado de acceder a una posición en una matriz de bytes, como por ejemplo \texttt{matr[0][0]}.

Para mostrar la forma en que definimos las expresiones del lenguaje, veamos el ejemplo de las expresiones de números enteros, a las cuales llamamos \textit{expresiones aritméticas}. Las expresiones aritméticas nos permiten representar números enteros y sobre ellos aplicar las operaciones de suma, resta, multiplicación, división y modulo de números enteros; ya sean literales o variables que contengan números enteros.

La forma de definirlas es inductivamente, partiendo de números literales y variables como casos base y luego construyendo expresiones más complejas a partir de ellos. Un ejemplo de expresión compleja es la multiplicación, ya que para construir una expresión de multiplicación es necesario primero contar con dos expresiones aritméticas, las cuales a su vez pueden ser resultados de otras operaciones ---incluyendo la misma multiplicación--- y de esta forma continuar en la recursión hasta llegar a los casos base.

Veamos entonces una definición más formal de algunas de las expresiones aritméticas en forma inductiva.
\begin{lstlisting}[mathescape, caption=Definición de algunas expresiones aritméticas.]
ArithExp := 
  arith_exp_num  : Integer  $\rightarrow$ ArithExp
  arith_exp_id   : Id       $\rightarrow$ ArithExp
  arith_exp_mult : ArithExp $\rightarrow$ ArithExp $\rightarrow$ ArithExp
\end{lstlisting}
Aquí se puede ver como los constructores base \texttt{arith\_exp\_num} y \texttt{arith\_exp\_id} no requieren de otra expresión aritmética y nos devuelven una expresión válida.
A partir de estos constructores y contando con variables y/o enteros literales, podemos construir expresiones aritméticas como por ejemplo \texttt{arith\_exp\_mult (arith\_exp\_num 3) (arith\_exp\_id x)}. Utilizando la notación del cuadro~\ref{notacion:arith_exp} del anexo \ref{subsec:apendice_sintaxis} se puede escribir la misma expresión más naturalmente como \texttt{3 * x}.

Las expresiones de tipo \texttt{Bool} tienen una definición muy similar a la de las expresiones aritméticas ya que la lógica de la definición es la misma. Al igual que para los números enteros, para los booleanos los casos base son los literales y las variables, pero en los casos inductivos podemos encontrar más variedad, aunque no más complejidad. La diferencia es que dentro de las expresiones booleanas hay algunas que se construyen a partir de expresiones de otros tipos, en particular expresiones aritméticas. Ejemplos de ello son la comparación entre enteros o bytes, que se construyen a partir de un par de expresiones aritméticas o un par de expresiones de byte respectivamente. En el siguiente fragmento se pueden ver algunos ejemplos.
\begin{lstlisting}[mathescape, caption=El tipo de las expresiones booleanas.]
BoolExp := 
  bool_exp_lit : Bool     $\rightarrow$ BoolExp
  bool_exp_id  : Id       $\rightarrow$ BoolExp
  bool_exp_lt  : ArithExp $\rightarrow$ ArithExp $\rightarrow$ BoolExp
  bool_exp_gtb : ByteExp  $\rightarrow$ ByteExp  $\rightarrow$ BoolExp
  bool_exp_not : BoolExp  $\rightarrow$ BoolExp
\end{lstlisting}
Un ejemplo de expresión booleana es el siguiente: \texttt{bool\_exp\_not (bool\_exp\_lt (arith\_exp\_num 3) (arith\_exp\_id x))} . Que al ser reescrito utilizando la notación del cuadro~\ref{notacion:bool_exp} del anexo \ref{subsec:apendice_sintaxis} queda \texttt{!(3 <\ 4)}.

Las expresiones de bytes y de matrices son análogas y se definen de la misma forma que lo hicimos con las expresiones aquí mostradas. Un ejemplo de expresión de byte es \texttt{byte\_exp\_shiftr (byte\_exp\_matrix matr (arith\_exp\_num 0) (arith\_exp\_num 1)) (arith\_exp\_num 1)}. O más simplemente utilizando la notación del cuadro~\ref{notacion:byte_exp} del anexo \ref{subsec:apendice_sintaxis}: \texttt{matr[0][1] shr 1}.
Y finalmente dos ejemplos de expresión de matriz: \texttt{matrix\_exp\_id mid} y \texttt{matrix\_exp\_init (arith\_exp\_num 2) (arith\_exp\_id two)}.

En el anexo~\ref{subsec:apendice_sintaxis} se puede ver la definición formal completa del lenguaje, allí la notación utilizada es muy similar a la de Coq ya que es casi directamente lo que se encuentra en el código fuente.

\subsubsection{Instrucciones}
Las expresiones por si mismas representan un valor, ya sea expresado por ejemplo como una operación matemática o como el valor almacenado en memoria de una variable, pero para escribir programas que realmente puedan realizar tareas útiles es necesario contar con instrucciones, las cuales nos permitirán alterar el estado de la memoria y así generar efectos visibles externamente.

Estas instrucciones determinan acciones a realizar, que al ser ejecutadas podrán transformar el estado de la memoria de distintas formas. Definimos entonces un conjunto básico de instrucciones el cual nos permitirá operar de manera eficaz teniendo como objetivo los algoritmos AES y Mini-AES.

A continuación veremos una a una las instrucciones junto con su notación.

\paragraph{Skip}
Esta es la más sencilla de las instrucciones ya que al ser ejecutada no realiza ninguna acción. Puede resultar inútil desde el punto de vista de un programador, pero la utilizamos para algunas estructuras internas al lenguaje. No tiene notación asignada y en caso de utilizarla simplemente se puede escribir \texttt{instr\_skip}.

\paragraph{Asignación}
Podríamos decir que la asignación es una de las instrucciones más importantes ya que al ser ejecutada esta modifica una posición en la memoria, de hecho junto con la modificación de posiciones de matrices, estas son las únicas instrucciones que modifican la memoria.

Más adelante veremos que al evaluar dicha instrucción se hará efectivo el cambio en la memoria pero en cuanto a sintaxis la asignación consta sencillamente de un tipo, una variable y una expresión del tipo dado.

Por ejemplo la asignación booleana se escribe de la siguiente forma:
\begin{lstlisting}
bool X ::= bexp;
\end{lstlisting}
Donde \texttt{X} es un identificador y \texttt{bexp} una expresión booleana.

La notación utilizada fue definida en Coq para que quien escriba un programa en este lenguaje pueda hacerlo de forma más clara, pero la forma de definir formalmente las instrucciones de asignación es de manera inductiva, al igual que las expresiones. En el anexo~\ref{subsec:apendice_instrucciones} se encuentra la definición formal de todas las instrucciones.

La asignación de enteros, bytes y matrices es análoga pero cambiando \texttt{bool} por \texttt{int}, \texttt{byte} o \texttt{matrix} respectivamente.

\paragraph{Modificación de una matriz}
Esta instrucción será de suma utilidad para nuestro algoritmo, la misma permite asignar un byte a una posición de un matriz, utilizando expresiones aritméticas para indicar la posición. La notación es la siguiente:
\begin{lstlisting}
matr[i][j] ::= bexp;
\end{lstlisting}
Donde \texttt{matr} es un identificador que contiene un valor de tipo \texttt{Matrix Byte}, \texttt{i} y \texttt{j} son expresiones aritméticas y \texttt{bexp} es una expresión de tipo \texttt{Byte}.

\paragraph{Instrucción condicional IFB}
Siendo la primera de las instrucciones de control, esta instrucción permite ejecutar un bloque de código en función de una condición booleana, sin ejecutar nada cuando la condición no se cumple. Este es un ejemplo en el que utilizamos la instrucción \texttt{instr\_skip}; para tener una sola implementación para el condicional con y sin alternativa \texttt{ELSE}. Entonces la notación para la instrucción es la siguiente:
\begin{lstlisting}
IFB bexp THEN
  instr;
END
\end{lstlisting}
Donde \texttt{bexp} es una expresión booleana e \texttt{instr} es una instrucción.

\paragraph{Instrucción condicional IFB THEN ELSE}
Esta es como la anterior pero se agrega la posibilidad de ejecutar un bloque de código si la condición no se cumple. La notación es la siguiente:
\begin{lstlisting}
IFB bexp THEN
  instr1;
ELSE
  instr2;
END
\end{lstlisting}
Donde \texttt{bexp} es una expresión booleana e \texttt{instr1} e \texttt{instr2} son instrucciones.

\paragraph{Instrucción WHILE}
Esta instrucción nos permite repetir una instrucción mientras se cumpla una condición booleana. El \texttt{WHILE} procederá a verificar el valor que contiene la condición booleana y ejecutará la instrucción en caso de ser verdadera, luego volverá a verificar la condición y ejecutar condicionalmente, así sucesivamente hasta que la condición contenga un valor falso. La notación para esta instrucción es la siguiente:
\begin{lstlisting}
WHILE bexp DO
  instr;
END
\end{lstlisting}
Donde \texttt{bexp} es una expresión booleana e \texttt{instr} es una instrucción o una secuencia de instrucciones.

\paragraph{Instrucción  FOR}
Esta instrucción es un caso especial de \texttt{WHILE} donde la condición siempre establece que el identificador pasado como parámetro contenga un valor menor o igual al límite establecido. Si bien para toda instrucción \texttt{FOR} existe una de tipo \texttt{WHILE} equivalente, resulta útil contar con una iteración más limitada evitando posibles errores de programación. La notación es la siguiente:
\begin{lstlisting}
FOR id TO aexp DO
  instr;
END
\end{lstlisting}
Donde \texttt{id} es un identificador que contiene un valor de tipo \texttt{Integer}, \texttt{aexp} es una expresión aritmética e \texttt{instr} es una instrucción o una secuencia de instrucciones.

\paragraph{Secuencia de instrucciones}
Como no tiene sentido en un lenguaje imperativo escribir programas de una sola instrucción, es necesario incluir una forma de ejecutar una instrucción luego de la otra. Para ello existe la secuencia de instrucciones, que toma como parámetros de forma inductiva dos instrucciones y devuelve una nueva instrucción. La notación para la secuencia es simplemente separar las instrucciones mediante punto y coma, solo que para unificar la notación utilizamos el punto y coma al final de todas las instrucciones aunque sea una sola o aunque sea la última de la secuencia. Este es otro caso en el que utilizamos la instrucción \texttt{skip} ya que cuando hay un punto y coma pero no sigue otra instrucción el lenguaje implícitamente agrega la instrucción \texttt{skip}. La notación es entoces:
\begin{lstlisting}
instr1;
instr2;
\end{lstlisting}
Donde \texttt{instr1} e \texttt{instr2} son instrucciones.

\subsection{Semántica}
Para poder dar semántica a nuestro lenguaje tenemos que definir cómo evaluamos las construcciones sintácticas. Al hablar de evaluación queremos decir la forma de ejecutar las instrucciones vistas en la parte anterior y, por consecuencia, también evaluar el resultado de las expresiones. Por ejemplo, supongamos que un programa contiene la siguiente instrucción:
\begin{lstlisting}
int x ::= 3 + y;
\end{lstlisting}
En un caso así será necesario utilizar la definición de cuatro tipos de evaluación para poder ejecutar la instrucción:
\begin{enumerate}
\item Evaluar el literal \texttt{3}
\item Evaluar la variable \texttt{y}
\item Evaluar el resultado de la suma
\item Evaluar la instrucción de asignación
\end{enumerate}

Para poder realizar estas definiciones utilizaremos los conceptos de \textit{estados} de memoria y \textit{transiciones} entre dichos estados mediante la evaluación de las instrucciones. Pero primero vamos a definir \textit{valores}, que serán el contenido de las posiciones en la memoria.

\subsubsection{Valores}
Los valores son los que ocupan las posiciones en memoria y, además de guardar el contenido en si mismo, también los marcamos con el tipo correspondiente. Definimos formalmente el tipo \texttt{Val} como:
\begin{lstlisting}[mathescape, caption=El tipo de los valores.]
Val :=
  bool_val        : Bool    $\rightarrow$ Val
  int_val         : Integer $\rightarrow$ Val
  byte_val        : Byte    $\rightarrow$ Val
  byte_matrix_val : $\forall$ (m n: $\mathbb{N}$), Matrix Byte m n $\rightarrow$ Val
\end{lstlisting}

De esta forma cuando leamos un valor de la memoria obtendremos por ejemplo \texttt{int\_val 9} indicando el tipo entero y el número correspondiente.

\subsubsection{Estado} \label{subsec:estado}
Un estado representa los valores de todas las variables en un momento dado. Siguiendo la definición de la memoria como la vimos en la sección~\ref{subsec:identificadores}, si la memoria es un arreglo de posiciones, entonces un estado es como una imagen de dicho arreglo en un determinado momento. Utilizando el estado podemos \textit{leer} la memoria, es decir que dado un identificador, un estado nos devuelve el valor correspondiente para esa variable en un determinado momento de la ejecución.
Por lo tanto definimos a cada estado como una función que toma un identificador y devuelve su valor, formalmente:
\begin{lstlisting}[mathescape, caption=El tipo del estado.]
State := Id $\rightarrow$ option Val
\end{lstlisting}
La función de estado no es total ya que no existe un valor correspondiente a una variable no definida, por eso el tipo de retorno es \texttt{option}, que puede ser \texttt{None} cuando la variable no está definida o \texttt{Some val} donde \texttt{val} es el valor correspondiente.

Definimos un estado vacío, en el cual no hay variables definidas, de la siguiente forma:
\begin{lstlisting}[mathescape, caption=Definición del estado vacío.]
empty_state: State := _ $\Rightarrow$ None
\end{lstlisting}
Este estado nos será de utilidad para poder realizar una definición recursiva de los estados.

Por último tenemos que definir una función que nos permita modificar el valor de una variable, definimos la siguiente función:
\begin{lstlisting}[mathescape, caption=Definición de una función para actualizar el estado., emph={if,then,else},emphstyle={\color{blue}\bfseries}, label=def:update]
update(st: State)(id: Id)(val: Val) : State :=
  (id': Id) $\Rightarrow$ if (equal_id id id') then Some val else st id'
\end{lstlisting}
La función \texttt{update} toma como parámetro un estado y retorna uno nuevo, para el cual se encuentra definido el identificador junto con su valor que también fueron pasados como parámetros. El nuevo estado entonces, toma como parámetro un identificador y se fija si éste es el mismo que fue escrito utilizando \texttt{update}, en cuyo caso simplemente debe retornar el valor correspondiente; en caso contrario delega la respuesta al estado original utilizado para la definición ---es aquí donde será de utilidad \texttt{empty\_state} para poder finalizar las llamadas recursivas.

La función \texttt{equal\_id} simplemente compara identificadores y la mantenemos en una definición abstracta para evitar depender de su implementación.

Las palabras clave \texttt{if}, \texttt{then} y \texttt{else} fueron resaltadas especialmente para evitar confusión ya que esta no es la instrucción de nuestro lenguaje, sino que es el condicional de Coq.

Veamos un ejemplo de un estado que puede llegar a ser construido usando estas primitivas. El siguiente estado contiene dos variables definidas mediante los identificadores \texttt{id 1} e \texttt{id 2} y sus valores correspondientes son \texttt{int\_val 2} y \texttt{bool\_val TRUE} respectivamente.
\begin{lstlisting}
update (update empty_state (id 2) (bool_val TRUE)) (id 1) (int_val 2)
\end{lstlisting}

Llamémosle \texttt{st} a dicho estado, si queremos leer el valor que se encuentra identificado por \texttt{id 2} debemos aplicar la función de estado, esto es, \texttt{st (id 2)}. Para ver su funcionamiento reducimos la expresión con la definición mostrada en \ref{def:update}:
\begin{lstlisting}[caption=Ejemplo de aplicación de la función de estado.]
st (id 2)
=
if (equal_id (id 1) (id 2)) then Some (int_val 2)
else (update empty_state (id 2) (bool_val TRUE)) (id 2)
=
if (false) then Some (int_val 2)
else (update empty_state (id 2) (bool_val TRUE)) (id 2)
=
(update empty_state (id 2) (bool_val TRUE)) (id 2)
=
if (equal_id (id 2) (id 2)) then Some (bool_val TRUE)
else emtpy_state (id 2)
=
if (true) then Some (bool_val TRUE)
else emtpy_state (id 2)
=
Some (bool_val TRUE)
\end{lstlisting}

Notar que si hubiéramos querido obtener el valor de una variable que nunca fue definida, la reducción hubiera continuado hasta llegar a \texttt{empty\_state}, que no importa el parámetro que tome siempre retorna \texttt{None}.

\subsubsection{Evaluación}
La evaluación de las instrucciones es la que determina realmente la ejecución de un programa, es aquí donde definimos cómo cada instrucción del lenguaje ---dependiendo de la evaluación de sus expresiones internas--- lleva de un estado a otro.

Veremos primero la evaluación de las expresiones aritméticas, booleanas, bytes y matrices antes de pasar a las instrucciones. Nuestra forma de definir la evaluación de dichas expresiones es mediante una relación entre la expresión, el estado y su valor. Diremos que una expresión evalúa a un cierto valor en un cierto estado si y solamente si la terna (expresión, estado, valor) se encuentra en la relación. Esto nos permite definir nuestra semántica mediante relaciones inductivas. Por ejemplo, siendo $\mathbb{S}$ el conjunto de todos los posibles estados de memoria, las expresiones aritméticas literales se evalúan de la siguiente forma:

\[
\forall (z \in \mathbb{Z}, st \in \mathbb{S}),\ st(id)\ =\ Some\ (int\_val\ z)\ \rightarrow (arith\_exp\_id \ z,\ st,\ z) \in ArithEval
\]

En las subsecciones a continuación asumiremos la existencia de un estado \texttt{st} y utilizaremos la notación \texttt{exp $\Downarrow$ val} para decir que la expresión \texttt{exp} evalúa al valor \texttt{val} en el estado \texttt{st}.

\subsubsection{Evaluación de expresiones}
Las siguientes tres, son las definiciones formales de evaluación de literal, identificador y multiplicación aritmética.
\begin{lstlisting}[mathescape, caption=Relación que define la evaluación de expresiones aritméticas.]
ArithEval :=
  arith_eval_num   : $\forall$ (n: Integer),
      arith_exp_num n $\Downarrow$ n

  arith_eval_id    : $\forall$ (i: Id)(z: Integer),
      st i = Some (int_val z) $\rightarrow$ arith_exp_id i $\Downarrow$  z

  arith_eval_mult  : $\forall$ (e1 e2: ArithExp) (n1 n2: Integer), 
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 * e2 $\Downarrow$ int_mult n1 n2
\end{lstlisting}
Notar que la evaluación de identificadores es la traducción del ejemplo visto en la sección anterior. Desde el punto de vista semántico, la evaluación de un identificador se realiza leyendo dicho valor en la memoria.

Como puede observarse, la evaluación de un literal aritmético vale directamente el valor del número entero y la evaluación de un identificador corresponde al valor que se encuentra en esa posición de memoria ---representada por el estado \texttt{st}--- siempre y cuando dicha variable se encuentre definida en \texttt{st}. La multiplicación primero evalúa el resultado de sus dos operandos y luego evalúa la operación de multiplicación en sí misma, aquí es donde utilizamos las operaciones abstractas mencionadas al comienzo de la sección, en este caso \texttt{int\_mult} cuyos detalles de implementación pueden ser sustituidos sin tener que cambiar nuestra definición de evaluación. Como ya fue dicho, en nuestro trabajo utilizamos las primitivas de Coq, entre las cuales se encuentran los números enteros y su multiplicación.

El resto de las expresiones se comporta de una forma muy similar y se puede leer su definición completa en el anexo~\ref{subsec:apendice_semantica}, sin embargo mostraremos algunos otros ejemplos que resultan interesantes y pueden ayudar a una mejor comprensión de la semántica. Veamos algunas definiciones de evaluación de expresiones de bytes:

\begin{lstlisting}[mathescape, caption=Relación que define la evaluación de expresiones de bytes.]
ByteEval :=
  byte_eval_lit : $\forall$ (b:Byte),
      byte_exp_num b $\Downarrow$ b

  byte_eval_id : $\forall$ (i:Id)(b:Byte),
      st i = Some (byte_val b) $\rightarrow$ byte_exp_id i $\Downarrow$ b

  byte_eval_shiftl : $\forall$ (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      e $\Downarrow$ b $\rightarrow$ n $\Downarrow$ x $\rightarrow$ e shl n $\Downarrow$ byte_shl b x

  byte_eval_matrix :
      $\forall$ (e1 e2: ArithExp) (m n i j: Integer)
        (mexp: MatrixExp) (matr: Matrix Byte m n),
     mexp $\Downarrow$ matr $\rightarrow$ e1 $\Downarrow$ i $\rightarrow$ e2 $\Downarrow$ j $\rightarrow$ mexp[e1][e2] $\Downarrow$ matrix_get i j matr
\end{lstlisting}

En el caso de las expresiones de bytes se aplica el mismo razonamiento para los literales y los identificadores. Por otro lado se puede notar que la operación de shift debe tomar como parámetros un byte y un entero, cada expresión evalúa al correspondiente valor de su tipo y luego la expresión completa evalúa al resultado de la operación abstracta \texttt{byte\_shl}. El último constructor corresponde al acceso a una posición de una matriz, éste consta de una expresión de matriz junto con dos expresiones aritméticas que representan el índice al cual se está accediendo. Por la forma en que definimos nuestro módulo de matrices, que será explicado en la sección~\ref{subsec:matrices}, en el caso de que la posición no se encuentre definida en la matriz, como por ejemplo un intento de acceso fuera de los límites de su tamaño, la operación \texttt{matrix\_get} retorna \texttt{None}.

\subsubsection{Evaluación de instrucciones}
En esta sección vamos a definir qué queremos decir con  evaluar una instrucción. Ejecutar una instrucción nos lleva de un estado de la memoria a otro, por lo que definimos la evaluación de una instrucción como una relación entre un estado inicial, una instrucción y el estado luego de ejecutar la misma. Podemos plantear un ejemplo similar al de la evaluación de expresiones en cuanto a relación inductiva; la siguiente es la definición de evaluación de asignación de enteros:

\[
\forall (zexp \in ArithExp,\ z \in\ \mathbb{Z}),\ zexp \Downarrow z\ \rightarrow (int\ x\ ::=\ zexp,\ st,\ st[x\leftarrow z]) \in InstrEval
\]

Donde se puede notar que al pertenecer la terna (instrucción, estado inicial, estado final) a la evaluación de instrucciones, entonces dicha instrucción al ser ejecutada realiza la transición del estado inicial al final.
La notación \texttt{st[x $\leftarrow$ z]} es equivalente a \texttt{update st x z}, función vista en la sección~\ref{subsec:estado} y quiere decir que es el mismo estado \texttt{st} donde escribimos el valor \texttt{z} en la variable \texttt{x}.

A continuación mostramos algunos ejemplos de la definición formal de la evaluación de instrucciones como tipo inductivo. En los lugares en que utilizamos una evaluación de expresión, por ejemplo \texttt{bexp $\Downarrow$ TRUE}, estamos referenciando implícitamente al único estado que es nombrado dentro del constructor y que en todos los casos se llama \texttt{st}. También utilizamos la notación \texttt{instr / st $\Downarrow$ st'} donde \texttt{instr} es la instrucción y \texttt{st} y \texttt{st'} son el estado inicial y final respectivamente.

\paragraph{Skip}
Esta instrucción no tiene ningún efecto sobre el estado, por lo tanto nos lleva de un estado \texttt{st} al mismo estado \texttt{st}.
\begin{lstlisting}[mathescape]
skip_eval :
  instr_skip / st $\Downarrow$ st
\end{lstlisting}

\paragraph{Asignación}
Esta instrucción toma como parámetros un identificador y una expresión y nos lleva de un estado \texttt{st} a un estado \texttt{st'}, donde \texttt{st'} es el resultado de en el estado \texttt{st} asignarle al identificador el valor de la expresión.
\begin{lstlisting}[mathescape]
assign_int_eval : $\forall$ (zid: Id) (zexp: ArithExp) (z: Integer),
  zexp $\Downarrow$ z $\rightarrow$ int zid ::= zexp / st $\Downarrow$ st[zid $\leftarrow$ z]
\end{lstlisting}
El ejemplo corresponde a la asignación de enteros pero es análoga para booleanos, bytes y matrices. La definición completa se puede ver en el anexo~\ref{subsec:apendice_semantica}


\paragraph{Instrucción de secuencia}
Esta instrucción se evalúa a partir de la evaluación de dos instrucciones. Toma como parámetro una instrucción \texttt{i1} que nos lleva de un estado \texttt{st} a uno \texttt{st'}, y una instrucción \texttt{i2} que nos lleva de un estado \texttt{st'} a uno \texttt{st''}. Por lo tanto esta instrucción nos lleva de un estado \texttt{st} a uno \texttt{st''}.
\begin{lstlisting}[mathescape]
seq_eval : $\forall$ (i1 i2: Instr) (st' st'': State),
  i1 / st $\Downarrow$ st' $\rightarrow$ i2 / st' $\Downarrow$ st'' $\rightarrow$ i1 ; i2 / st $\Downarrow$ st''
\end{lstlisting}

\paragraph{Instrucción IF}
Esta instrucción recibe como parámetro una expresión booleana y dos instrucciones \texttt{i1} e \texttt{i2}. Realizamos la evaluación dependiendo si el resultado de evaluar la expresión booleana es verdadero o falso, esto se puede ver en los dos constructores \texttt{if\_eval\_true} y \texttt{if\_eval\_false}. En el primer caso, el resultado es verdadero y esta instrucción nos lleva del estado \texttt{st} al \texttt{st'} ejecutando la instrucción \texttt{i1}, en el segundo caso el resultado es falso por lo que la instrucción nos lleva del estado \texttt{st} a otro estado \texttt{st'} ejecutando la instrucción \texttt{i2}.
\begin{lstlisting}[mathescape]
if_eval_true : $\forall$ (bexp: BoolExp) (i1 i2 : Instr) (st': State),
    bexp $\Downarrow$ TRUE $\rightarrow$ i1 / st $\Downarrow$ st' $\rightarrow$
    IF bexp THEN i1 ELSE i2 END / st $\Downarrow$ st'

if_eval_false : $\forall$ (bexp: BoolExp) (i1 i2: Instr) (st': State),
    bexp $\Downarrow$ FALSE $\rightarrow$ i2 / st $\Downarrow$ st' $\rightarrow$
    IF bexp THEN i1 ELSE i2 END / st $\Downarrow$ st'
\end{lstlisting}

\paragraph{Instrucción WHILE}
Esta instrucción recibe como parámetro una expresión booleana y una instrucción. Realizamos la evaluación dependiendo si el resultado de evaluar la expresión booleana es verdadero o falso, por lo cual necesitamos dos constructores los cuales son \texttt{while\_eval\_true} y \texttt{while\_eval\_flase}. Si el resultado es verdadero esta instrucción nos lleva del estado \texttt{st} al \texttt{st'} ejecutando la instrucción \texttt{i}, y en ese estado \texttt{st'} nos lleva al estado \texttt{st''} volviendo a ejecutar el loop. Si el resultado de evaluar la expresión es falso nos deja en el mismo estado inicial \texttt{st}.
\begin{lstlisting}[mathescape]
while_eval_true : $\forall$ (bexp: BoolExp) (i: Instr) (st' st'': State),
    bexp $\Downarrow$ TRUE $\rightarrow$ i / st $\Downarrow$ st' $\rightarrow$
    WHILE bexp DO i END / st' $\Downarrow$ st'' $\rightarrow$
    WHILE bexp DO i END / st $\Downarrow$ st''

while_eval_false : $\forall$ (bexp: BoolExp) (i: Instr),
    bexp $\Downarrow$ FALSE $\rightarrow$ WHILE bexp DO i END / st $\Downarrow$ st
\end{lstlisting}

\paragraph{Instrucción FOR}
Esta instrucción recibe como parámetro un identificador con una variable de tipo entero, una expresión aritmética y una instrucción. Realizamos la evaluación dependiendo si el valor de la variable es mayor o igual que el valor de la expresión artimética, separando en dos casos: \texttt{for\_eval\_step} y \texttt{for\_eval\_end}. Si el resultado es mayor o igual, esto es \texttt{for\_eval\_end}, nos quedamos en el mismo estado. Si es menor, pasamos del estado \texttt{st} al \texttt{st''}, sabiendo que, ejecutando una vez la instrucción ---cuerpo del for--- pasamos del estado \texttt{st} al estado \texttt{st'}. Partiendo del estado \texttt{st'} y ejecutando el for con la variable de control incrementada en uno pasamos del estado \texttt{st} al \texttt{st''}.
\begin{lstlisting}[mathescape]
for_eval_end : $\forall$ (i: Id) (n: Integer) (instr: Instr),
    i $\geq$ n $\Downarrow$ TRUE $\rightarrow$ FOR i TO n DO instr END / st $\Downarrow$ st

for_eval_step : $\forall$ (i: Id) (x n: Integer)
                  (instr: Instr) (st' st'': State),
    i < n $\Downarrow$ TRUE $\rightarrow$ instr / st $\Downarrow$ st' $\rightarrow$ 
    FOR i TO n DO instr END / st' $\Downarrow$ st'' $\rightarrow$
    st' i = Some (int_val x) $\rightarrow$
    st'' i = Some (int _val (x + ONE)) $\rightarrow$
    FOR i TO n DO instr END / st $\Downarrow$ st''
\end{lstlisting}

\paragraph{Instrucción SET Matrix}
Esta instrucción recibe como parámetro un identificador que contiene la matriz a la que se le quiere setear un elemento, dos expresiónes aritmetícas que representan los índices de la matriz, y el byte que se desea setear. En la relación se exige que el resultado de aplicar la función que modifica el valor de la matriz sea válido, es decir que el resultado sea de tipo \texttt{Some}, luego la evaluación de la instrucción nos lleva del estado inicial \texttt{st} a un estado igual pero donde la variable que contenía la matriz inicial ahora contiene la matriz luego de modificar la posición especificada por los índices, con el byte pasado como parámetro.
\begin{lstlisting}[mathescape]
matrix_set_eval : $\forall$ (m n i j: Integer) (e1 e2: ArithExp) (e: ByteExp)
                    (mid: Id) (matr matr': Matrix Byte m n) (b: Byte),
    mid $\Downarrow$ matr $\rightarrow$ e1 $\Downarrow$ i $\rightarrow$ e2 $\Downarrow$ j $\rightarrow$ e $\Downarrow$ b $\rightarrow$ 
    matrix_set matr i j b = Some matr' $\rightarrow$
    mid[e1][e2] ::= e / st $\Downarrow$ st[mid $\leftarrow$ matr']
\end{lstlisting}


\subsection{Matrices} \label{subsec:matrices}
Para poder implementar los algoritmos AES y Mini-AES necesitamos contar con un tipo de dato para las matrices. Como la librería estándar de Coq no cuenta con este tipo, intentamos utilizar una implementación existente \cite{Matrices} pero su enfoque no resultó útil para este trabajo. Decidimos entonces implementar nuestro propio módulo de matrices. Este módulo nos permite definir matrices de tamaño y tipo paramétricos, y cuenta con los respectivos operadores \texttt{get} y \texttt{set}. También en este módulo desmostramos ciertas propiedades sobre las matrices que serán utilizadas en la prueba de corrección del Mini-AES.

\subsubsection{Representación}
Representamos una matriz de tamaño $m \times n$ como un vector de largo $m$, donde cada posición del mismo es a su vez un vector de largo $n$ correspondiéndose con una fila de la matriz. Implementamos estos vectores en Coq como listas con tipo paramétrico y dependientes en el tamaño, sea \texttt{A} un tipo de datos cualquiera, definimos un vector de la siguiente forma:
\begin{lstlisting}[mathescape, caption=Definición inductiva de vectores.]
vect A :=
  vnil  : vect A 0
  vcons : $\forall$ (n: $\mathbb{N}$), A $\rightarrow$ vect A n $\rightarrow$ vect A (Suc n)
\end{lstlisting}

Luego la definición de matriz $m \times n$ es:
\begin{lstlisting}[mathescape, caption=Definición del tipo de las matrices.]
Matrix A (m n: $\mathbb{N}$) := vect (vect A m) n
\end{lstlisting}

\subsubsection{Operaciones}
En este módulo de matrices implementamos las operaciones \texttt{get}, \texttt{set} y \texttt{new\_matr} que se corresponden con las operaciones \texttt{matrix\_get}, \texttt{matrix\_set} y \texttt{matrix\_zero}, las cuales fueron definidas abstractamente en la sintaxis del lenguaje.

La función \texttt{get} retorna el valor correspondiente a la posición indicada por los índices \texttt{i} y \texttt{j}:
\begin{lstlisting}[mathescape, caption=Firma de get.]
get (A: Set)(m n i j: $\mathbb{N}$)(matr: Matrix A m n): option A
\end{lstlisting}

Por otro lado, \texttt{set} retorna una nueva mariz que contiene a \texttt{elem} en la posición indicada por los índices \texttt{i} y \texttt{j}:
\begin{lstlisting}[mathescape, caption=Firma de set.]
set (A:Set)(m n i j: $\mathbb{N}$)(elem: A)(matr: Matrix A m n): option (Matrix A n m)
\end{lstlisting}

Tanto \texttt{get} como \texttt{set} retornan un opcional para indicar el caso de fallo. Para ambas funciones, la única precondición para que retornen un valor de tipo \texttt{Some} es:
\[
(0\ \leq\ i\ \leq\ m-1)\ \land\ (0\ \leq\ j\ \leq\ n-1)
\]
Y esto es debido a que los índices varían desde $0$ hasta $n-1$ siendo $n$ el largo del vector.

La función \texttt{new\_matr} genera una nueva matriz de \texttt{m} filas por \texttt{n} columnas donde todas sus posiciones contienen al valor \texttt{elem} :
\begin{lstlisting}[mathescape, caption=Firma de new\_matr.]
new_matr (A: Set)(elem: A)(m n: $\mathbb{N}$): Matrix A n m
\end{lstlisting}

\subsubsection{Propiedades sobre Matrices}
Como vimos en la sección anterior, las operaciones \texttt{get} y \texttt{set} requieren ciertas precondiciones para no fallar, en cuyo caso retornan \texttt{None}. Resulta interesante por otro lado verificar que en el caso de cumplirse las precondiciones entonces el resultado es el esperado.

Para el acceso a una posición, basta con probar que siempre que el tamaño de la matriz sea válido y los índices de acceso se encuentren en un rango también válido, entonces existe un resultado. Enunciamos esto mediante el lema \textbf{get\_some}:
\begin{align*}
\forall\ (i\ j\ m\ n:\ \mathbb{N})\ &(matr:\ Matrix\ A\ m\ n),\\
&m \geq 1\ \rightarrow\ n \geq 1\ \rightarrow\ 0 \leq i < m\ \rightarrow\ 0 \leq j < n\ \rightarrow\ \exists\ a,\ matr[i][j]\ =\ Some\ a
\end{align*}
  
Al modificar una posición, nos interesa comprobar que siempre que modifiquemos una posición válida debe existir una matriz como resultado de la operación. El lema \textbf{set\_matrix} expresa dicho comportamiento:
\begin{align*}
\forall\ (i\ j\ m\ n:\ \mathbb{N})\ &(matr:\ Matrix\ A\ m\ n)\ (b:\ A),\\
&0 \leq i < m\ \rightarrow\ 0 \leq j < n\ \rightarrow\ \exists\ matr',\ (matr[i][j]\ ::=\ b)\ =\ Some\ matr'
\end{align*}

Una vez probados estos dos lemas, necesitamos profundizar más y probar que al modificar una posición en una matriz y luego acceder a la misma posición obtenemos el valor modificado. Para ello demostramos el lema  \textbf{set\_matrix\_get}:
\begin{align*}
\forall\ (i\ j\ m\ n:\ \mathbb{N})\ &(matr\ matr':\ Matrix\ A\ m\ n)\ (a:\ A), \\
&m \geq 1\ \rightarrow\ n \geq 1\ \rightarrow\ 0 \leq i < m\ \rightarrow\ 0 \leq j < n\ \rightarrow\ \\
&(matr[i][j]\ ::=\ a)\ =\ Some\ matr'\ \rightarrow\ matr'[i][j]\ =\ Some\ a
\end{align*}

Finalmente nos resultó útil contar con un lema que nos garantice que al modificar una posición en una matriz, las demás posiciones no varían. Para ello demostramos que si modificamos una posición y luego accedemos a otra posición distinta, el valor obtenido es el mismo que se encontraba en la matriz inicial. A este lema lo llamamos \textbf{get\_set\_other\_matrix\_get}:
\begin{align*}
\forall\ (i\ j\ q\ s\ m\ n:\ \mathbb{N})\ &(matr\ matr':\ Matrix\ A\ m\ n)\ (a\ b:\ A), \\
                        &0 \leq i < m\ \rightarrow\ 0 \leq j < n\ \rightarrow \\
                        &0 \leq q < m\ \rightarrow\ 0 \leq s < n\ \rightarrow \\
                        &\lnot (i\ =\ q\ \land\ j\ =\ s)\ \rightarrow \\
                        &matr[i][j]\ =\ Some\ a\ \rightarrow \\
                        &(matr[q][s]\ ::=\ b)\ =\ Some\ matr'\ \rightarrow \\
                        &matr'[i][j]\ =\ Some\ a
\end{align*}

\clearpage


%--------------------- AES ---------------------%
\section{AES}
\label{sec:aes}
En esta sección veremos de forma más detallada el funcionamiento de AES, así como también la versión simplificada del mismo.

\subsection{Aritmética de cuerpos finitos}
Este algoritmo se basa fundamentalmente en la teoría de campos finitos, que puede ser estudiada en mayor profundidad en \cite{campos_finitos}. Sin embargo, introducimos aquí brevemente las nociones fundamentales para comprender la operativa de AES.\\

Un \textit{cuerpo} es un conjunto de elementos junto con la definición dos operaciones llamadas \textit{adición} y \textit{multiplicación}, que cumplen las propiedades asociativa, conmutativa y distributiva de la multiplicación respecto de la adición. A partir de dichas operaciones se debe poder definir un inverso aditivo y otro multiplicativo así como un elemento neutro para la adición y uno para la multiplicación. Estos elementos permiten efectuar las operaciones de sustracción y división. Un \textit{cuerpo finito} es por definición un \textit{cuerpo} definido sobre un conjunto finito de elementos.

Un byte puede ser interpretado como un elemento de un cuerpo finito si usamos una representación polinomial. Sea un byte $b$ definido por sus ocho bits $b_i,\ 0 \leq i \leq 7$, su representación polinomial es la siguiente:
\[
b_7x^7+b_6x^6+b_5x^5+b_4x^4+b_3x^3+b_2x^2+b_1x+b_0
\]

Por ejemplo el byte $10010111$ identifica el elemento $x^7+x^4+x^2+x+1$ del cuerpo finito.

Definimos entonces las operaciones de adición y multiplicación que, además de ser necesarias para la definición del cuerpo finito, serán aplicadas por las operaciones del algoritmo y resultan de importancia para nuestro trabajo.

\paragraph{Adición}
La suma de dos elementos en este cuerpo finito se logra sumando cada coeficiente utilizando la suma exclusiva, también conocida como XOR y para la cual utilizaremos la notación $\oplus$. Esta operación es muy económica de implementar en hardware y es muy utilizada en AES, sus cuatro posibles resultados son: $1 \oplus 1 = 0$, $1 \oplus 0 = 1$, $0 \oplus 1 = 1$ y $0 \oplus 0 = 0$. Para todo par de bytes $a$ y $b$ entonces se define la adición $c$ como $c_i = a_i \oplus b_i,\ 0 \leq i \leq 7$.

Por ejemplo el siguiente es el resultado de una adición en el cuerpo finito:
\[
(x^6+x^4+x^2+1) \oplus (x^7+x^6+x^5+x^4) = x^7+x^5+x^2+1
\]

Que puede ser representado en la notación binaria de bytes como:
\[
01010101 \oplus 11110000 = 10100101
\]

\paragraph{Multiplicación}
En esta representación polinómica de bytes, la multiplicación se define igual que la multiplicación de polinomios pero tomando el resultado módulo un polinomio irreducible de grado 8. Un polinomio es irreducible si sus únicos divisores son 1 y él mismo, y en este cuerpo finito que estamos estudiando existen varios que cumplen dicha condición. Su justificación puede encontrarse en \cite{rijndael_libro} y por lo tanto no la veremos aquí, pero para AES fue elegido como polinomio irreducible para utilizar en las operaciones el siguiente: $x^8+x^4+x^3+x+1$. Utilizaremos la notación $\bullet$ para referirnos a esta operación.

Por ejemplo podemos realizar la siguiente multiplicación:
\begin{align*}
&(x^6+x^4+x^2+x+1) \bullet (x^7+x+1)\ = \\
&(x^{13}+x^{11}+x^9+x^8+x^7)+(x^7+x^5+x^3+x^2+x)+x^6+x^4+x^2+x+1\ = \\
&x^{13}+x^{11}+x^9+x^8+x^6+x^5+x^4+x^3+1
\end{align*}
Y al reducirla módulo el polinomio irreducible:
\[
(x^{13}+x^{11}+x^9+x^8+x^6+x^5+x^4+x^3+1)\ mod\ (x^8+x^4+x^3+x+1)\ =\ x^7+x^6+1
\]

Esta reducción nos garantiza que el resultado siempre será de grado menor o igual a 7 y por lo tanto pertenece al cuerpo finito. Existen demostraciones de que efectivamente el cuerpo finito aquí definido cumple las propiedades requeridas, para más detalle ver \cite{campos_finitos}. Este cuerpo finito tiene un nombre que es $GF(2^8)$ y será el nombre que utilizaremos en adelante.

\paragraph{Rijndael S-box}
La \textit{S-box} (substitution box) de Rijndael es una matriz cuadrada de tamaño 16 por 16 bytes que será utilizada por el algortimo para proveer no linealidad. Como veremos en algunas operaciones, esta se utiliza como tabla de búsqueda, es decir que será utilizada como una función que dado un byte retorna otro. Utilizaremos en este documento una notación similar a la aplicación de funciones, por ejemplo \texttt{S-box(b)} es el byte correspondiente a \texttt{b}, aunque la operación real que se está realizando es buscar la posición $i,j$ de la matriz donde $i$ se obtiene de los 4 bits de mayor orden y $j$ de los siguientes 4; por ejemplo para el byte $11001100$ el correspondiente es el byte en la posición $12,12$ de la matriz S-box.

Esta matriz fue diseñada para que el algoritmo sea resistente a criptoanálisis lineal y diferencial, la forma de generarla así como una mejor explicación de sus fundamentos de resistencia al criptoanálisis pueden verse en detalle en \cite{rijndael_libro}.

\subsection{Rijndael}
Como ya fue mencionado previamente, AES trabaja sobre bloques de la entrada, aplicando varias rondas de distintas operaciones sobre cada uno de ellos, por lo cual se caracteriza como una red de sustitución-permutación.

\begin{table}[ht]
	\centering
	\begin{tabular}{|c|c|c|}
		\hline
		\textbf{Tamaño de la clave (bits)} & \textbf{Cantidad de rondas} & \textbf{Nk} \\ \hline
		128 & 10 & 4 \\ \hline
		192 & 12 & 6 \\ \hline
		256 & 14 & 8 \\
		\hline
	\end{tabular}
	\caption{Cantidad de rondas dependiendo del tamaño de la clave.}
	\label{tab:cant_rondas}
\end{table}

Como puede apreciarse en la tabla~\ref{tab:cant_rondas}, se aplican 10, 12 o 14 rondas para claves de 128, 192 o 256 bits respectivamente; el valor de \texttt{Nk} será mejor comprendido al ver la sección~\ref{subsec:exp_clave}. Nos concentraremos en ver las operaciones que se realizan a un único bloque, sin perder generalidad ya que el proceso aplicado a cada uno de ellos es exactamente el mismo. Dicho bloque se representa como una matriz de 4 filas por 4 columnas de bytes y de aquí en adelante nos referiremos a éste como \textit{matriz de estado} o simplemente \textit{estado}.
Como veremos más adelante, una de las operaciones a aplicar en cada ronda depende de la clave, pero es requerido que en cada una la clave sea diferente. Por dicho motivo existe un paso previo a la encriptación misma del texto, que es la \textit{expansión de la clave}, donde a partir de la clave inicial, se genera una clave nueva para cada ronda.

Los algoritmos \ref{lst:pseudo_aes_encrypt} y \ref{lst:pseudo_aes_decrypt} muestran en alto nivel el orden en que son aplicadas las operaciones sobre el estado. El parámetro \texttt{state} representa la matriz de estado y por lo tanto es una matriz de 4 por 4 bytes, mientras que \texttt{key} es la clave expandida, que es representada como un arreglo de largo \texttt{Nr+1} donde cada entrada del mismo es a su vez una matriz de exactamente el mismo tamaño y tipo que la matriz de estado. La constante \texttt{Nr} contiene el número de rondas que deben ser aplicadas y es dependiente del tamaño de la clave.

\begin{algorithm}[ht]
\caption{AES encrypt}
\label{lst:pseudo_aes_encrypt}
\begin{algorithmic}
\Procedure{aes\_encrypt}{$state, sbox, key$}
	\State \Call{add\_round\_key}{$state, key[0]$}
	\For{round = 1 to Nr-1}
		\State \Call{sub\_bytes}{$state, sbox$}
		\State \Call{shift\_rows}{$state$}
		\State \Call{mix\_columns}{$state$}
		\State \Call{add\_round\_key}{$state, key[round]$}
	\EndFor
	\State \Call{sub\_bytes}{$state, sbox$}
	\State \Call{shift\_rows}{$state$}
	\State \Call{add\_round\_key}{$state, key[Nr]$}
\EndProcedure
\end{algorithmic}
\end{algorithm}
\begin{algorithm}[ht]
\caption{AES decrypt}
\label{lst:pseudo_aes_decrypt}
\begin{algorithmic}
\Procedure{aes\_decrypt}{$state, sboxInv, key$}
	\State \Call{add\_round\_key}{$state, key[0]$}
	\For{round = 1 to Nr-1}
		\State \Call{sub\_bytes}{$state, sboxInv$}
		\State \Call{inv\_shift\_rows}{$state$}
		\State \Call{inv\_mix\_columns}{$state$}
		\State \Call{add\_round\_key}{$state, key[round]$}
	\EndFor
	\State \Call{sub\_bytes}{$state, sboxInv$}
	\State \Call{inv\_shift\_rows}{$state$}
	\State \Call{add\_round\_key}{$state, key[Nr]$}
\EndProcedure
\end{algorithmic}
\end{algorithm}

En la figura~\ref{fig:aes} mostramos un diagrama de \cite{Stallings} que muestra claramente la aplicación de cada paso del algoritmo al estado y donde se puede ver cómo los procedimientos de encriptar y desencriptar realizan las operaciones inversas en el orden exactamente inverso.

\begin{figure}[ht]
\centering
\includegraphics[scale=1.2]{img/AES.jpg}
\caption{Diagrama de funcionamiento de AES \cite{Stallings}.}
\label{fig:aes}
\end{figure}

A continuación mostramos la expansión de la clave así como cada una de las operaciones referenciadas en el pseudocódigo.
\subsubsection{Expansión de la clave}
\label{subsec:exp_clave}
\begin{algorithm}[ht]
\caption{AES key expansion}
\label{lst:exp_clave}
\begin{algorithmic}
\Procedure{key\_expansion}{initial\_key, expanded\_key}
	\For{$i = 0$ to $Nk-1$}
	    \State $expanded\_key[i] \gets initial\_key[i]$
	\EndFor
	\For{$i \gets Nk$ to $4*(Nr+1)-1$}
	    \State $temp \gets expanded\_key[i-1]$
	    \If{$i \% 4 = 0$}
	        \State \Call{rot\_word}{$temp$}
	        \State \Call{sub\_word}{$temp$}
	        \State $temp[0] \gets temp[0] \oplus Rcon(i/Nk)$
	    \ElsIf{$Nk > 6$ and $i\%Nk = 4$}
	            \State \Call{sub\_word}{$temp$}
	    \EndIf
	    \State $expanded\_key[i] \gets expanded\_key[i-Nk] \oplus temp$
	\EndFor
\EndProcedure
\end{algorithmic}
\end{algorithm}

En el algoritmo~\ref{lst:exp_clave} se puede observar la forma de expandir la clave. Este toma como argumento la clave inicial que es una matriz de 4 filas y \texttt{Nk} columnas de bytes y escribe en \texttt{expanded\_key}, la clave expandida, que es una matriz de 4 filas y $4*(Nr+1)$ columnas de bytes. Para simplificar la notación, tomamos los accesos a las matrices de forma que retornen la $i$-ésima columna comenzando en 0; por ejemplo \texttt{expanded\_key[0]} retorna la primera columna, que son 4 bytes, de \texttt{expanded\_key}.
En el primer \texttt{for} simplemente se copia la clave inicial al principio de la expandida y en el segundo se generan las columnas restantes, obteniendo $Nr+1$ claves de 4 por 4 bytes, que es el tamaño del bloque.
Dado que la cantidad de filas es fija y vale 4, se puede calcular el valor de \texttt{Nk} en función del tamaño de la clave. Por ejemplo para una clave de 128 bits, que son 16 bytes, debemos dividirlos en 4 filas y el resultado es 4 columnas. El resto de los resultados se encuentra en la tabla~\ref{tab:cant_rondas}.

\subsubsection*{RotWord}
Este procedimiento simplemente toma una palabra de 32 bits ---que puede ser vista como un arreglo de 4 bytes--- y los rota 8 posiciones a la izquierda ---o 1 sola si son vistos como bytes. Se puede ver claramente en un ejemplo, si la entrada a \texttt{RotWord} es una tira de bits escrita en forma hexadecimal como $2A00F110$ entonces el resultado sería $00F1102A$.

\subsubsection*{SubWord}
\label{subsec:sub_word}
Dada una entrada de 4 bytes, \texttt{SubWord} reemplaza cada uno de dichos bytes por su correspondiente en la \texttt{S-box}. Por lo tanto podemos definir al procedimiento de la siguiente forma:
\begin{equation*}
\texttt{SubWord(in) = [S-box(in[0]), S-box(in[1]), S-box(in[2]), S-box(in[3])]}
\end{equation*}
Siendo \texttt{in} un arreglo de 4 bytes.

\subsubsection*{Rcon}
Esta operación se puede especificar de la siguiente forma:
\begin{equation*}
Rcon(i) = x\textsuperscript{i-1} \bmod x^8 + x^4 + x^3 + x + 1
\end{equation*}
La exponenciación es realizada en el cuerpo finito $GF(2^8)$.
En la práctica se necesita como máximo el valor de $Rcon(10)$ para una clave de 128 bits, $Rcon(8)$ y $Rcon(7)$ para 192 y 256 bits respectivamente. Por lo tanto es sencillo de implementar con una tabla de búsqueda con máximo 10 posiciones distintas.

\subsubsection{Procedimiento AddRoundKey}
En \texttt{AddRoundKey} lo que se hace es combinar la clave con el estado. Esto sirve para lograr que la clave afecte la salida del algoritmo y, combinado con el resto de las operaciones, se producirá el efecto deseado de que al cambiar una pequeña parte de la clave esto afecte la mayor parte de la salida.
\begin{algorithm}[ht]
\caption{AddRoundKey}
\label{lst:add_round_key}
\begin{algorithmic}
\Procedure{add\_round\_key}{state, key}
	\For{$i = 0$ to $3$}
	    \For{$j = 0$ to $3$}
	        \State $state[i][j] \gets state[i][j] \oplus key[i][j]$
        \EndFor
	\EndFor
\EndProcedure
\end{algorithmic}
\end{algorithm}
El algoritmo~\ref{lst:add_round_key} muestra en alto nivel el funcionamiento del procedimiento. Cada posición $i,j$ es un byte y la operación $\oplus$ retorna el \texttt{XOR} bit a bit.

A la hora de desencriptar un texto cifrado se utiliza esta misma operación ya que se cumple $\forall a,\ a \oplus a = 0$ y $\forall a,\ a \oplus 0 = a$, y por lo tanto se cumple $\forall a\ b,\ a \oplus b \oplus b = a$, lo cual indica que aplicar AddRoundKey dos veces con la misma clave nos devuelve el texto inicial.

\subsubsection{Procedimiento SubBytes}
Este procedimiento, que puede ser observado en el algoritmo~\ref{lst:sub_bytes}, sustituye cada byte del estado por su correspondiente en la operación de sustitución implementada por la tabla de búsqueda \texttt{S-Box} y funciona de la misma forma que el procedimiento \texttt{SubWord} de la expansión de la clave, explicado en la sección~\ref{subsec:sub_word}. El objetivo de esta operación es claramente aportar no linealidad al algoritmo debido a las propiedades ya mencionadas de la tabla de sustitución.

La operación inversa que se realiza para desencriptar es exactamente la misma en cuanto al algoritmo, pero la tabla de búsqueda que se usa contiene los valores que corresponden a la función inversa de \texttt{S-box}.
\begin{algorithm}[ht]
\caption{SubBytes}
\label{lst:sub_bytes}
\begin{algorithmic}
\Procedure{sub\_bytes}{state, sbox}
	\For{$i = 0$ to $3$}
	    \For{$j = 0$ to $3$}
	        \State $state[i][j] \gets $ \Call{$sbox$}{$state[i][j]$}
        \EndFor
	\EndFor
\EndProcedure
\end{algorithmic}
\end{algorithm}

\subsubsection{Procedimiento ShiftRows}
Si nos fijamos hasta ahora las operaciones que fueron vistas afectan las cuatro columnas de bytes del estado de manera independiente, lo cual degeneraría en cuatro algoritmos que aplican operaciones a las columnas independientemente en lugar de al bloque completo, por lo cual el algoritmo no produciría los efectos de confusión y difusión. Para lograr estos efectos, se transforma la matriz de estado rotando a la izquierda cada fila, tantas veces como el número mismo de la fila. De esta forma un cambio en el texto de entrada o en la clave se distribuye en la salida generando confusión y difusión.
\begin{algorithm}[ht]
\caption{ShiftRows}
\label{lst:shift_rows}
\begin{algorithmic}
\Procedure{shift\_rows}{state}
	\For{$i = 0$ to $3$}
        \State \Call{$shift$}{$state, i$}
	\EndFor
\EndProcedure
\Procedure{shift}{$state, n$}
    \For{$i = 0$ to $n$}
        \State $aux \gets state[i][0]$
        \State $state[i][0] \gets state[i][1]$
        \State $state[i][1] \gets state[i][2]$
        \State $state[i][2] \gets state[i][3]$
        \State $state[i][3] \gets aux$
    \EndFor
\EndProcedure
\end{algorithmic}
\end{algorithm}

Se puede ver en el algoritmo~\ref{lst:shift_rows} cada fila $i$ es rotada a la izquierda $i$ veces, notar que la primera fila cuyo índice es $0$ no es rotada en absoluto. Cabe notar que pueden haber implementaciones más eficientes pero aquí estamos mostrando el funcionamiento conceptual del algoritmo.

La operación inversa a ShiftRows utilizada para desencriptar ---denominada $INV\_SHIFT\_ROWS$ en el algoritmo~\ref{lst:pseudo_aes_decrypt}--- funciona de la misma forma a excepción de que las rotaciones se realizan a la derecha, por lo cual componer ShiftRows con su inversa trivialmente mantienen a la entrada sin modificar.

\subsubsection{Procedimiento MixColumns}
Esta operación junto con ShiftRows aporta a generar difusión, ya que al aplicarla los cuatro valores de cada columna de la entrada se combinan para formar cada valor de la salida. Para ello el procedimiento consiste en multiplicar cada columna por una matriz fija que es la siguiente:
\[
\begin{bmatrix}
   2 & 3 & 1 & 1 \\
   1 & 2 & 3 & 1 \\
   1 & 1 & 2 & 3 \\
   3 & 1 & 1 & 2
\end{bmatrix}
\]
Aunque su fundamento se encuentra mejor explicado en \cite{rijndael_libro}, podemos mencionar que esta matriz fue elegida especialmente para asegurar la mezcla de los bytes de cada columna y después de pocas rondas al combinarse con ShiftRows, todos los bits de la salida dependerán de todos los bits de la entrada. Además sus coeficientes fueron elegidos teniendo en cuenta su implementación, ya que con estos coeficientes la multiplicación puede implicar como máximo un shift y un XOR de bytes.

\begin{algorithm}[ht]
\caption{MixColumns}
\label{lst:mix_columns}
\begin{algorithmic}
\Procedure{mix\_columns}{state}
	\For{$i = 0$ to $3$}
        \State \Call{$mix$}{$state[i]$}
	\EndFor
\EndProcedure
\Procedure{mix}{$state$}
    \State $state[0] \gets (2 \bullet state[0]) \oplus (3 \bullet state[1]) \oplus state[2] \oplus state[3]$
    \State $state[1] \gets state[0] \oplus (2 \bullet state[1]) \oplus (3 \bullet state[2]) \oplus state[3]$
    \State $state[2] \gets state[0] \oplus state[1] \oplus (2 \bullet state[2]) \oplus (3 \bullet state[3])$
    \State $state[3] \gets (3 \bullet state[0]) \oplus state[1] \oplus state[2] \oplus (2 \bullet state[3])$
\EndProcedure
\end{algorithmic}
\end{algorithm}

El algoritmo~\ref{lst:mix_columns} resume el funcionamiento indicado. Al igual que se ha tratado hasta ahora, la multiplicación y la suma se interpretan en el cuerpo finito $GF(2^8)$ y por eso los símbolos $\bullet$ y $\oplus$.

Para el procedimiento de desencriptar se realiza la misma operación a diferencia de la matriz de multiplicación ---$INV\_MIX\_COLUMNS$ en el algoritmo~\ref{lst:pseudo_aes_decrypt}, en cuyo caso es la siguiente:
\[
\begin{bmatrix}
   0E & 0B & 0D & 09 \\
   09 & 0E & 0B & 0D \\
   0D & 09 & 0E & 0B \\
   0B & 0D & 09 & 0E
\end{bmatrix}
\]

Si realizamos la multiplicación entre ambas matrices obtenemos la siguiente igualdad:
\[
\begin{bmatrix}
   0E & 0B & 0D & 09 \\
   09 & 0E & 0B & 0D \\
   0D & 09 & 0E & 0B \\
   0B & 0D & 09 & 0E
\end{bmatrix}
\bullet
\begin{bmatrix}
   02 & 03 & 01 & 01 \\
   01 & 02 & 03 & 01 \\
   01 & 01 & 02 & 03 \\
   03 & 01 & 01 & 02
\end{bmatrix}
=
\begin{bmatrix}
   01 & 00 & 00 & 00 \\
   00 & 01 & 00 & 00 \\
   00 & 00 & 01 & 00 \\
   00 & 00 & 00 & 01
\end{bmatrix}
\]

Lo cual implica que ambas operaciones son inversas y al componerlas la salida resulta igual a la entrada.

\subsection{Mini-AES}
\label{subsec:mini_aes}

\subsubsection{Algoritmo}
Por ser una simplificación del AES, el algoritmo Mini-AES funciona de la misma forma pero aplicándose en bloques de menor tamaño y utilizando una clave de menor tamaño además de aplicar menor cantidad de rondas. Para el estudio del Mini-AES nos centraremos entonces en sus diferencias con el original.
\\
El tamaño de cada bloque y, por lo tanto, de la matriz de estado en el Mini-AES es de 16 bits. Tanto el estado como la clave consisten en matrices de 2 filas por 2 columnas y, en lugar de contener cada posición un byte, estas contienen unidades de 4 bits denominadas \textit{nibble}s. El número de rondas es exactamente 2 y, al igual que en el AES original, en la última ronda no se aplica la transformación \texttt{MixColumns}.


\begin{algorithm}[ht]
\caption{Mini-AES encrypt}
\label{lst:mini_aes_encrypt}
\begin{algorithmic}
\Procedure{encrypt}{$state, sbox, multTable, key$}
	\State \Call{key\_addition}{$state, key[2]$}
	
	\State \Call{nibble\_sub}{$state, sbox$}
	\State \Call{shift\_row}{$state$}
	\State \Call{mix\_column}{$state, multTable$}
	\State \Call{key\_addition}{$state, key[1]$}
	
	\State \Call{nibble\_sub}{$state, sbox$}
	\State \Call{shift\_row}{$state$}
	\State \Call{key\_addition}{$state, key[0]$}
\EndProcedure
\end{algorithmic}
\end{algorithm}

\begin{algorithm}[ht]
\caption{Mini-AES decrypt}
\label{lst:mini_aes_decrypt}
\begin{algorithmic}
\Procedure{decrypt}{$state, sboxInv, multTable, key$}
	\State \Call{key\_addition}{$state, key[0]$}
	\State \Call{shift\_row}{$state$}
	\State \Call{nibble\_sub}{$state, sboxInv$}
	\State \Call{key\_addition}{$state, key[1]$}
	\State \Call{mix\_column}{$state, multTable$}
	\State \Call{shift\_row}{$state$}
	\State \Call{nibble\_sub}{$state, sboxInv$}
	\State \Call{key\_addition}{$state, key[2]$}
\EndProcedure
\end{algorithmic}
\end{algorithm}



En los algoritmos \ref{lst:mini_aes_encrypt} y \ref{lst:mini_aes_decrypt} mostramos el funcionamiento en alto nivel del Mini-AES, allí se puede observar que éste ejecuta solamente 2 rondas de transformaciones. Describimos al mismo aplicando las transformaciones una a una. Como veremos de aquí en adelante, cada transformación se verá simplificada debido al tamaño reducido de la matriz de estado.

\subsubsection{Expansión de la clave}
\begin{algorithm}[ht]
\caption{Mini-AES key expansion}
\label{lst:mini_exp_clave}
\begin{algorithmic}
\Procedure{mini\_key\_expansion}{init\_key, exp\_key}
    \State $exp\_key[0][0] \gets init\_key[0][0]$
    \State $exp\_key[0][1] \gets init\_key[0][1]$
    \State $exp\_key[1][0] \gets init\_key[1][0]$
    \State $exp\_key[1][1] \gets init\_key[1][1]$
    \\
	\State $exp\_key[0][2] \gets exp\_key[0][0] \oplus$ \Call{nibble\_sub}{exp\_key[1][1]} $\oplus Rcon(1)$
    \State $exp\_key[0][3] \gets exp\_key[0][1] \oplus exp\_key[0][2]$
    \State $exp\_key[1][2] \gets exp\_key[1][0] \oplus exp\_key[0][3]$
    \State $exp\_key[1][3] \gets exp\_key[1][1] \oplus exp\_key[1][2]$
    \\
    \State $exp\_key[0][4] \gets exp\_key[0][2] \oplus$ \Call{nibble\_sub}{exp\_key[1][3]} $\oplus Rcon(2)$
    \State $exp\_key[0][5] \gets exp\_key[0][3] \oplus exp\_key[0][4]$
    \State $exp\_key[1][4] \gets exp\_key[1][2] \oplus exp\_key[0][5]$
    \State $exp\_key[1][5] \gets exp\_key[1][3] \oplus exp\_key[1][4]$
\EndProcedure
\end{algorithmic}
\end{algorithm}
Al igual que en el AES, la primera parte de la clave expandida es la misma que la clave de entrada al algoritmo general, luego dos claves más son generadas, una para cada ronda. Se utilizan las transformaciones \texttt{NibbleSub} y \texttt{Rcon}, la primera es la equivalente a \texttt{SubBytes} y será explicada más adelante mientras que la segunda ya fue explicada en la sección~\ref{subsec:exp_clave} donde se habla de la expansión de la clave. El algoritmo~\ref{lst:mini_exp_clave} muestra paso a paso la expansión de cada posición de la clave.

\subsubsection{Procedimiento KeyAddition}
Siendo análoga a \texttt{AddRoundKey}, en esta transformación, como se puede observar en el algoritmo~\ref{lst:key_addition}, se aplica \texttt{XOR} con la clave correspondiente en cada una de las entradas de la matriz de estado.
\begin{algorithm}[ht]
\caption{KeyAddition}
\label{lst:key_addition}
\begin{algorithmic}
\Procedure{key\_addition}{state, key}
    \State $state[0][0] \gets state[0][0] \oplus key[0][0]$
    \State $state[0][1] \gets state[0][1] \oplus key[0][1]$
    \State $state[1][0] \gets state[1][0] \oplus key[1][0]$
    \State $state[1][1] \gets state[1][1] \oplus key[1][1]$
\EndProcedure
\end{algorithmic}
\end{algorithm}
Al igual que en AES, esta operación es inversa de si misma y por lo tanto se usa en encrypt y decrypt.

\subsubsection{Procedimiento NibbleSub}
Esta es la transformación equivalente a \texttt{SubBytes} y se realiza de la misma forma, sustituyendo en la matriz de estado cada entrada por su correspondiente en la \texttt{S-box}, podemos observar la {S-box} en el cuadro ~\ref{tab:mini_sbox} y su inversa en el cuadro ~\ref{tab:mini_sboxinv}. La única diferencia aquí es que la tabla tiene un tamaño menor y como podemos observar en el algoritmo~\ref{lst:nibble_sub} escribimos la sustitución de cada entrada de la matriz en una sentencia sin usar bucles.
\begin{algorithm}[ht]
\caption{Nibble sub}
\label{lst:nibble_sub}
\begin{algorithmic}
\Procedure{nibble\_sub}{state, sbox}
    \State $state[0][0] \gets $ \Call{$sbox$}{$state[0][0]$}
    \State $state[0][1] \gets $ \Call{$sbox$}{$state[0][1]$}
    \State $state[1][0] \gets $ \Call{$sbox$}{$state[1][0]$}
    \State $state[1][1] \gets $ \Call{$sbox$}{$state[1][1]$}
\EndProcedure
\end{algorithmic}
\end{algorithm}

\input{Mini-S-Box}

\input{Mini-S-BoxInv}


Para desencriptar, la operación que se utiliza es la misma pero cambiando la \texttt{S-box} por otra que es exactamente la inversa.

\subsubsection{Procedimiento ShiftRow}
En \texttt{ShiftRow} se realiza la rotación de filas al igual que en la original \texttt{ShiftRows}. Notar que la diferencia en el nombre es simplemente pasar a singular debido a que, al tener solamente 2 filas la matriz, solamente se termina rotando una fila ---recordar que la primera fila, cuyo índice es 0, no es rotada.
Podemos implementar esta transformación simplemente como un \texttt{swap} entre las dos entradas de la segunda fila de la matriz, como se muestra en el algoritmo~\ref{lst:shift_row}.
\begin{algorithm}[ht]
\caption{Shift row}
\label{lst:shift_row}
\begin{algorithmic}
\Procedure{shift\_row}{state, sbox}
    \State $aux \gets state[1][0]$
    \State $state[1][0] \gets state[1][1]$
    \State $state[1][1] \gets aux$
\EndProcedure
\end{algorithmic}
\end{algorithm}

Como finalmente esta operación es un intercambio de posiciones, ella es inversa de sí misma y para desencriptar no es necesario implementar otra función inversa.

\subsubsection{Procedimiento MixColumns}
En esta transformación se aplica lo mismo que en la original \texttt{MixColumns} pero con una matriz más reducida que es la siguiente:
\[
\begin{bmatrix}
   3 & 2 \\
   2 & 3
\end{bmatrix}
\]
Debido a que los posibles valores de entrada no son demasiados y para simplificar la implementación de esta operación, decidimos implementar la función mediante una tabla de búsqueda. Esta tabla abstrae la función $multTable(i,j) = (3 \bullet i) \oplus (2 \bullet j)$. Notar que como la operación $\oplus$ es conmutativa, si damos vuelta los índices tenemos $multTable(j,i) = (2 \bullet i) \oplus (3 \bullet j)$. Entonces \texttt{MixColumns} puede ser implementado como en el algoritmo~\ref{lst:mini_mix_columns}.
\begin{algorithm}[ht]
\caption{Mix columns}
\label{lst:mini_mix_columns}
\begin{algorithmic}
\Procedure{mix\_columns}{state, multTable}
    \State $aux00 \gets state[0][0]$
    \State $aux10 \gets state[1][0]$
    \State $state[0][0] \gets$ \Call{$multTable$}{$aux00, aux10$}
    \State $state[1][0] \gets$ \Call{$multTable$}{$aux10, aux00$}
    \\
    \State $aux01 \gets state[0][1]$
    \State $aux11 \gets state[1][1]$
    \State $state[0][1] \gets$ \Call{$multTable$}{$aux01, aux11$}
    \State $state[1][1] \gets$ \Call{$multTable$}{$aux11, aux01$}
\EndProcedure
\end{algorithmic}
\end{algorithm}

Esta tabla en particular cumple una propiedad que más adelante será importante:
\begin{align*}
		multTable(x_1,\ y_1)\ =\ x_2\ &\land\ multTable(y_1,\ x_1)\ =\ y_2 \\
		&\rightarrow \\
		multTable(x_2,\ y_2)\ =\ x_1\ &\land\ multTable(y_2,\ x_2)\ =\ y_1
\end{align*}

Lo cual quiere decir que la misma tabla se utilizará para la operación \texttt{MixColumns} así como para su operación inversa al desencriptar.


%------------------- Mini-AES ------------------%

\subsection{Implementación de Mini-AES}
A continuación veremos una a una las traducciones de los pseudocódigos vistos en la sección~\ref{subsec:mini_aes} a código Coq utilizando nuestro lenguaje. Podrá apreciarse una transformación bastante directa y sencilla. Por la naturaleza imperativa del lenguaje y por la forma de funcionar del algoritmo que ya fue explicada previamente, todos los procedimientos reciben como entrada un identificador que apunta a la variable donde se encuentra la matriz de estado y modifican la misma en el lugar.

\subsubsection{Procedimiento KeyAddition}
Este procedimiento se puede escribir de forma casi idéntica al pseudocódigo, utilizamos las notaciones de acceso a una posición de matriz, operación de xor y asignación a posiciones de matriz.

Los parámetros \texttt{text} y \texttt{key} son identificadores que contienen la matriz de estado y la clave respectivamente.
\begin{lstlisting}
Definition key_addition(text key: Id) :=
  text[0][0] ::= text[0][0] xor key[0][0];
  text[0][1] ::= text[0][1] xor key[0][1];
  text[1][0] ::= text[1][0] xor key[1][0];
  text[1][1] ::= text[1][1] xor key[1][1];
.
\end{lstlisting}

\subsubsection{Procedimiento Nibble sub}
Es acá donde se pueden encontrar mayores diferencias con el pseudocódigo. Para poder obtener el valor correspondiente a un byte en la tabla de sustitución \texttt{sbox}, necesitamos primero guardar el byte original en una variable. Esto se debe a que la posición de una matriz se indexa utilizando expresiones aritméticas y no bytes. Si quisiéramos acceder directamente, por ejemplo \texttt{sbox[0][text[0][0]]} tendríamos un error sintáctico ya que \texttt{text[0][0]} es una expresión de byte. Por el contrario, los identificadores sirven tanto como expresiones de bytes así como aritméticas, de esta forma guardamos un valor que es un byte, que luego será leido como número entero para acceder a la matriz.

Los parámetros \texttt{text} y \texttt{sbox} son identificadores que contienen la matriz de estado y la tabla de sustitución respectivamente.
\begin{lstlisting}
Definition nibble_sub (text sbox: Id) :=
  byte a00   ::= text[0][0];
  byte b00   ::= sbox[0][a00];
  text[0][0] ::= b00;

  byte a01   ::= text[0][1];
  byte b01   ::= sbox[0][a01];
  text[0][1] ::= b01;

  byte a10   ::= text[1][0];
  byte b10   ::= sbox[0][a10];
  text[1][0] ::= b10;

  byte a11   ::= text[1][1];
  byte b11   ::= sbox[0][a11];
  text[1][1] ::= b11;
.
\end{lstlisting}

\subsubsection{Procedimiento Shift row}
Este es el procedimiento más sencillo, solo requiere el parámetro \texttt{text} que contiene a la matriz de estado. La traducción a nuestro lenguaje es directa.
\begin{lstlisting}
Definition shift_row (text : Id) :=
  byte aux   ::= text[1][0];
  text[1][0] ::= text[1][1];
  text[1][1] ::= aux;
.
\end{lstlisting}

\subsubsection{Procedimiento Mix columns}
En \texttt{mix\_columns} nuevamente tenemos el problema de acceder a una posición de matriz utilizando el resultado de un acceso a matriz previo. Es por ello que también aquí utilizamos variables auxiliares donde almacenamos valores intermedios para poder realizar las sustituciones.

Los parámetros \texttt{text} y \texttt{mult\_table} son identificadores que contienen la matriz de estado y la tabla de multiplicación, respectivamente.
\begin{lstlisting}
Definition mix_columns (text mult_table: Id) :=
  byte a00   ::= text[0][0];
  byte a10   ::= text[1][0];
  text[0][0] ::= mult_table[a00][a10];
  text[1][0] ::= mult_table[a10][a00];

  byte a01   ::= text[0][1];
  byte a11   ::= text[1][1];
  text[0][1] ::= mult_table[a01][a11];
  text[1][1] ::= mult_table[a11][a01];
.
\end{lstlisting}

\subsubsection{Procedimiento Encrypt}
Para implementar el procedimiento de encriptación simplemente debemos hacer las llamadas correspondientes a los métodos definidos previamente. Para esto es necesario tener todos los parámetros que son exigidos por dichos procedimientos, estos son la matriz de estado ---inicialmente es el texto plano, la tabla de sustitución, la tabla de multiplicación y las tres claves que debieron ser generadas en una etapa de expansión de clave.
\begin{lstlisting}
Definition encrypt (text sbox mult_table key_0 key_1 key_2: Id) :=
  key_addition text key_2;
  nibble_sub   text sbox;
  shift_row    text;
  mix_columns  text mult_table;
  key_addition text key_1;
  nibble_sub   text sbox;
  shift_row    text;
  key_addition text key_0;
.
\end{lstlisting}

\subsubsection{Procedimiento Decrypt}
Al igual que al encriptar, al realizar el proceso inverso son necesarios todos los parámetros. Llamamos \texttt{cipher\_text} al texto cifrado que debió ser el resultado de aplicar \texttt{encrypt}, y llamamos \texttt{sbox\_inv} a la tabla de sustitución inversa a la utilizada para encriptar; \texttt{mult\_table} recibe el mismo nombre ya que ella es su propia tabla inversa. Las claves mantienen su nombre ya que para que esta operación cumpla la propiedad de ser inversa de la de encriptación, es necesario que sean exactamente las mismas claves.
\begin{lstlisting}
Definition decrypt (cipher_text sbox_inv mult_table
                    key_0 key_1 key_2: Id) :=
  key_addition cipher_text key_0;
  shift_row    cipher_text;
  nibble_sub   cipher_text sbox_inv;
  key_addition cipher_text key_1;
  mix_columns  cipher_text mult_table;
  shift_row    cipher_text;
  nibble_sub   cipher_text sbox_inv;
  key_addition cipher_text key_2;
.
\end{lstlisting}

\clearpage
%------------------- Logica de Hoare ------------------%
\section{Lógica de Hoare}
\label{sec:hoare}
La lógica de Hoare (también conocida como logica de Floyd-Hoare o Reglas de Hoare) es un sistema formal desarrollado por C.A.R. Hoare — y posteriormente refinado por otros investigadores — que proporciona un conjunto de reglas de inferencia para razonar sobre distintas propiedades (especialmente corrección y terminación) de programas imperativos con el rigor de la lógica matemática.

Esta lógica fue publicada por Hoare en 1969 en \cite{Hoare:1969:ABC:363235.363259} donde mencionó las contribuciones de Robert Floyd, que había publicado un sistema similar para los diagramas de flujo.

En este trabajo, utilizaremos la lógica de Hoare para probar la corrección del algoritmo Mini-AES. Una forma para poder determinar la corrección de un programa es hacer afirmaciones sobre los valores de determinadas variables en determinado punto de ejecución.

\subsection{Afirmaciones}
Para poder razonar sobre los programas necesitamos poder realizar afirmaciones sobre propiedades que cumplen los programas en un punto dado de ejecución, mas precisamente necesitamos poder realizar afirmaciones sobre el estado de la memoria en un punto dado del programa. Para esto definimos el siguiente tipo:
\[
  Assertion\ :=\ state\ \rightarrow\ Prop
\]

$Prop$ es en Coq el tipo de todas las proposiciones lógicas. Por ejemplo: $True$ y $False$ son proposiciones lógicas; así mismo, dadas dos proposiciones $A$ y $B$, se puede construir una nueva proposición $A \land B$, que semánticamente es la conjunción de $A$ y $B$. De esta forma y con todos los operadores vistos en la sección \ref{subsubsec:expresiones}, se definen todas las proposiciones lógicas. 

Diremos entonces que una afirmación es una familia de proposiciones lógicas indizadas por estado. Esto puede ser visto más claramente como una función que dado un estado retorna una propiedad sobre el mismo, escrita como proposición lógica. Esto nos resultara sumamente útil para poder definir pre y postcondiciones que se cumplen antes y después de ejecutar una o más instrucciones.

De aquí en adelante utilizaremos el término \textit{afirmación} para referirnos a una \textit{Assertion}.

\subsection{Ternas de Hoare}
El principal fundamento de esta lógica es la terna o triplete. Una terna describe como la ejecución de un bloque de código cambia el estado del programa. Las ternas tienen la siguiente forma: $\{P\}\ S\ \{Q\}$, donde $P$ y $Q$ son afirmaciones que deben cumplirse para que se cumpla la terna. Es decir, que si el programa $S$ comienza en un estado $st$ en el que se cumple $P$ ---lo cual quiere decir que se puede probar $P\ st$, entonces luego de ejecutar el programa, la memoria queda en un estado $st'$ para el cual se cumple $Q$, y por lo tanto se puede demostrar $Q\ st'$. A $P$ le llamamos precondición y a $Q$ postcondición.


\subsection{Reglas}
El objetivo de la lógica de Hoare es probar de manera composicional la validez de una terna. De esta forma, la estructura de la prueba debe reflejar la estructura del programa. A continuación vamos a introducir reglas para razonar sobre cada una de las instrucciones del lenguaje: asignación, condicional, loops, etc.

\subsubsection{Skip}
Si bien esta regla es sencilla, es necesario tenerla ya que contamos con una regla para cada una de las instrucciones del lenguaje y por lo tanto \texttt{skip} también cuenta con una. Esta regla nos dice que la instrucción \texttt{skip} no cambia el estado del programa. Por lo tanto si una proposición es válida antes de ejecutar la instrucción, también es válida después:
\[
\overline{\{ Q \}\ skip\ \{ Q \}}
\]

\subsubsection{Asignación}
Esta es la regla principal de la lógica de Hoare. Ella nos dice que, para que la propiedad $P$ sea válida en el estado siguiente a la asignación de una expresión a una variable, la propiedad debe ser válida en el estado anterior, pero sustituyendo todas las ocurrencias de la variable por la expresión. Dada una variable $X$ y una expresión $exp$ la regla tiene la siguiente forma:
\[
\overline{\{P [X\ \rightarrow\ exp]\}\ X\ ::=\ exp\ \{P\}}
\]
Donde $P [X\ \rightarrow\ exp]$ se lee como ``P en donde todas las ocurrencias de X se sustituyen por exp''. Los siguientes son ejemplos de ternas válidas:

\begin{itemize}
    \item $\{  x + 1 = 2 \} \   y := x + 1 \  \{ y = 2 \}$
    \item $\{  x + 1 \leq N \} \  x := x + 1  \ \{ x \leq N \}$
\end{itemize}

\subsubsection{Asignación de una posición de una matriz}
Es de fundamental importancia para este trabajo contar con una regla análoga a la de la asignación vista anteriormente, pero para la asignación de una posición de una matriz.

Supongamos que contamos con un identificador $mid$ cuyo valor en memoria es una matriz $matr$ y sabemos también que $set\ i\ j\ exp\ matr\ =\ matr'$ para cualquier par de enteros $i$ y $j$ y una expresión de byte $exp$.
Expresamos la regla de la siguiente forma:
\[
\overline{\{Q [mid\ \rightarrow\ matr']\}\ mid[i][j]\ ::=\ exp\ \{Q\}}
\]

Con esta regla, sabemos que $Q$ se cumple luego de ejecutar la instrucción si se cumplía también en el estado anterior pero sustituyendo las ocurrencias de $mid$ por $matr'$.\\

El siguiente es un ejemplo donde se puede aplicar la regla de la asignación de una posición de la matriz:\\

\[ \{ mid = \left( \begin{array}{cc}1 & m_{01}\\ m_{10} & m_{11}\end{array} \right) \} \ mid[0][0] := 1 \ \{ mid = \left( \begin{array}{cc}1 & m_{01}\\ m_{10} & m_{11}\end{array} \right) \}\]


\subsubsection{Secuencia}
Un programa está formado generalmente por una secuencia de instrucciones separadas por punto y coma, que se ejecutan una tras otra. La regla de la secuencia nos permite concatenar dos instrucciones, y obtener las pre y postcondiciones para la concatenación de ambas. Esta regla es fundamental para poder razonar sobre programas que cuentan con más de una instrucción.

Supongamos que tenemos una instrucción \texttt{i1} que nos lleva de un estado donde se cumple $P$ a un un estado donde se cumple $Q$. Supongamos también que tenemos otra instrucción \texttt{i2} que nos lleva de cualquier estado donde se cumple $Q$ a un estado donde se cumple $R$. Entonces si partimos de cualquier estado donde se cumple $P$ y ejecutamos \texttt{i1} seguido de \texttt{i2}, llegaremos a un estado donde se cumple $R$. Formalmente:\\
\begin{align*}
\{P\}\ i1\ \{Q\} \\
\{Q\}\ i2\ \{R\} \\
\overline{\ \{P\}\ i1;\ i2\ \{ R\}}
\end{align*}

Por ejemplo, consideremos la siguiente terna que cuenta con dos instrucciones:

\begin{itemize}
    \item $\{  x + 1 = 2 \} \   y := x + 1; z := y \  \{ z = 2 \}$
\end{itemize}

Podemos aplicar la regla de la secuencia, tomando Q = $\{ y = 2 \}$; esto nos lleva a tener que probar las siguientes dos ternas:

\begin{itemize}
    \item $\{  x + 1 = 2 \} \   y := x + 1 \  \{ y = 2 \}$
    \item $\{  y = 2 \} \  z := y  \ \{ z = 2 \}$
\end{itemize}


\subsubsection{Consecuencia}
A veces puede pasar que las precondiciones  o las postcondiciones que nos quedan en las reglas de Hoare no sean exactamente las que necesitamos, pero sean lógicamente equivalentes. En particular esto se da cuando tenemos una precondición más fuerte o una postcondición más débil. Para resolver este problema, formulamos las siguientes reglas:\\

\begin{displaymath}
    \frac{
      \begin{array}{ccc}
			\{\begin{array}{c}P'\end{array}\} & i & \{\begin{array}{c}Q\end{array}\}\\
			P & \rightarrow & P'
		\end{array}
    }{
	 	\begin{array}{lcr}
		\{\begin{array}{c}P \end{array}\} & i & \{\begin{array}{c}Q\end{array}\}
		\end{array}
    } \textrm{ (regla para la precondición)}
\end{displaymath}
\\

\begin{displaymath}
    \frac{
      \begin{array}{c}
		\left\{\begin{array}{c}P\end{array}\right\}
        \begin{array}{c}i\end{array}
        \left\{\begin{array}{l}Q'\end{array}\right\}        
        \\\begin{array}{c}Q'\end{array}
        \rightarrow
        \begin{array}{c}Q\end{array}
        
      \end{array}
    }{
      \left\{\begin{array}{c}P\end{array}\right\}
        \begin{array}{c}i\end{array}
        \left\{\begin{array}{c}Q\end{array}\right\}
    } \textrm{ (regla para la postcondición)}
\end{displaymath}
\\

Consideremos la siguiente terna:\\

$\{ 0 \leq x < 2 \}$ \texttt{x := x + 1} $\{ 0 \leq x \leq 2 \}$\\

Sabiendo que $0 \leq x \rightarrow -1 \leq x$, entonces podemos aplicar la regla para la precondicion, y esto nos lleva a tener que probar la siguiente terna:\\

$\{ -1 \leq x < 2 \}$ \texttt{x := x + 1} $\{ 0 \leq x \leq 2 \}$ que es lógicamente igual a \\

$\{ 0 \leq x +1 \leq 2 \}$ \texttt{x := x + 1} $\{ 0 \leq x \leq 2 \}$ que sabemos se cumple por la regla de la asignación.\\

Continuaremos ahora con el ejemplo para la regla de la postcondición. Consideremos la siguiente terna:\\

$\{ 0 \leq 2 \}$ \texttt{x := 0} $\{ x = 0 \}$\\

Sabiendo que $x = 0 \rightarrow x \leq 2$, entonces podemos aplicar la regla para la postcondición, y esto nos lleva a tener que probar la siguiente terna:\\

$\{ 0 \leq 2 \}$ \texttt{x := 0 } $\{ x \leq 2 \}$ que sabemos se cumple por la regla de la asignación.\\

\subsubsection{Condicional}
Dada una instrucción de la forma \texttt{IF b THEN i1 ELSE i2 END}, la regla para el \texttt{IF} dice que dada una postcondición $Q$ común a \texttt{i1} e \texttt{i2} entonces ésta es postcondición de la instrucción \texttt{IF}. Para la precondicion debemos considerar el caso en donde la condición del \texttt{IF} es verdadera y se ejecuta el cuerpo del \texttt{IF}, y el caso donde la condición es falsa y se ejecuta el cuerpo del \texttt{ELSE}. Por lo tanto, dada una precondicion $P$ y una expresión booleana \texttt{b}, consideramos como precondición del cuerpo del \texttt{IF} a la conjunción de $P$ y \texttt{b}, y como precondición del cuerpo del \texttt{ELSE} a la conjunción de $P$ y la negación de \texttt{b}, dando lugar a la siguiente regla:

\begin{displaymath}
    \frac{
      \begin{array}{c}
		\left\{\begin{array}{c}P  \wedge b\end{array}\right\}
        \begin{array}{c}i1\end{array}
        \left\{\begin{array}{l}Q\end{array}\right\} \\       
        \left\{\begin{array}{c}P \wedge \lnot b\end{array}\right\}
        \begin{array}{c}i2\end{array}
        \left\{\begin{array}{l}Q\end{array}\right\} 
        
      \end{array}
    }{
      \left\{\begin{array}{c}P\end{array}\right\}
        \begin{array}{c}\textrm{IF b THEN i1 ELSE i2}\end{array}
        \left\{\begin{array}{l}Q\end{array}\right\}
    } 
\end{displaymath}

Por ejemplo, supongamos que queremos probar lo siguiente:\\

 $\{ 0 \leq x \leq 2 \}$ \texttt{IFB x < 2 THEN x := x + 1 ELSE x := 0} $\{ 0 \leq x \leq 2 \}$\\

Aplicamos la regla condicional y luego debemos probar dos cosas:\\

 $\{ 0 \leq x \leq 2 \wedge x <2 \}$ \texttt{x := x + 1} $\{ 0 \leq x \leq 2 \}$, 
que simplificado nos queda:\\
 
 $\{ 0 \leq x < 2 \}$ \texttt{x := x + 1} $\{ 0 \leq x \leq 2 \}$ correspondiente al cuerpo del IF-THEN, y\\

 $\{ 0 \leq x \leq 2 \wedge x \geq 2 \}$ \texttt{x := 0 } $\{ 0 \leq x \leq 2 \}$, 
que simplificado nos queda:\\
 
 $\{ x = 2 \}$ \texttt{x := 0} $\{ 0 \leq x \leq 2 \}$ correspondiente al cuerpo del ELSE.


\subsubsection{While}
Dada una instrucción de la forma \texttt{WHILE b DO i END}, donde \texttt{b} es una expresión booleana e \texttt{i} es una instrucción o secuencia de instrucciones que representa el cuerpo del \texttt{WHILE}. Esta regla dice que: dada una condición $P$; sabiendo que antes del cuerpo del \texttt{WHILE} se cumple $P$ y \texttt{b} es verdadero, y después del cuerpo del \texttt{WHILE} también se cumple $P$, entonces podemos afirmar que $P$ se mantendrá invariante para cualquier número de repeticiones, por lo tanto sabemos que $P$ es precondición y postcondición de la instrucción \texttt{WHILE}, y ademas sabemos que al finalizar el \texttt{WHILE} el valor de \texttt{b} es falso.

\begin{displaymath}
    \dfrac{
      \begin{array}{c}
		\left\{\begin{array}{c}P \wedge b\end{array}\right\}
        \begin{array}{c}i\end{array}
        \left\{\begin{array}{l}P\end{array}\right\}        
      \end{array}
    }{
      \left\{\begin{array}{c}P\end{array}\right\}
        \begin{array}{c}\textrm{WHILE b DO i END}\end{array}
        \left\{\begin{array}{l}P \wedge \lnot b\end{array}\right\}
    } 
\end{displaymath}

Consideremos el siguiente ejemplo:\\

 $\{ x \leq 2 \}$ \texttt{WHILE x < 2 DO x := x + 1 END} $\{ x = 2\}$\\
 
 Sabiendo que $\neg x < 2 \wedge x \leq 2  \rightarrow x = 2$, aplicamos la regla para la postcondición, que nos lleva a tener que probar lo siguiente:\\
 
$\{ x \leq 2 \}$ \texttt{WHILE x < 2 DO x := x + 1 END} $\{\neg x < 2 \wedge x \leq 2 \}$\\

Donde ahora sí podemos aplicar la regla del \texttt{WHILE}, que nos lleva a tener que probar la siguiente terna:\\

$\{ x \leq 2 \wedge x < 2\}$ \texttt{x := x + 1} $\{ x \leq 2 \}$, que de forma simplificada nos queda:\\ 

$\{ x < 2\}$ \texttt{x := x + 1} $\{ x \leq 2 \}$, que es lógicamente equivalente a:\\


$\{ x + 1 \leq 2\}$ \texttt{x := x + 1} $\{ x \leq 2 \}$, que sabemos se cumple por la regla de la asignación.

 


\subsubsection{For}
Dada una instrucción de la forma \texttt{FOR i TO n DO instr END}, esta regla dice que si se cumple $i\ <\ n$ y $P$ es pre y postcondición de \texttt{instr}, entonces sabemos que $P$ es pre y postcondición de la instrucción \texttt{FOR}, y además sabemos que al finalizar la iteración el valor de $i$ es mayor o igual a $n$.
\begin{displaymath}
    \dfrac{
      \begin{array}{c}
		\left\{\begin{array}{c}P \wedge i < n\end{array}\right\}
        \begin{array}{c}instr\end{array}
        \left\{\begin{array}{l}P\end{array}\right\}        
      \end{array}
    }{
      \left\{\begin{array}{c}P\end{array}\right\}
        \begin{array}{c}\textrm{FOR i TO n DO instr END}\end{array}
        \left\{\begin{array}{l}P \wedge i \geq n\end{array}\right\}
    } 
\end{displaymath}

Consideremos el siguiente ejemplo:\\

 $\{ x \leq 2 \}$ \texttt{FOR x TO 2 DO y := y + x END} $\{ x = 2\}$\\
 
 Sabiendo que $x = 2  \rightarrow x \geq 2 \wedge x \leq 2$, aplicamos la regla para la postcondición, que nos lleva a tener que probar lo siguiente:\\
 
$\{ x \leq 2 \}$ \texttt{FOR x TO 2 DO y := y + x END} $\{\  x \geq 2 \wedge x \leq 2 \}$\\

donde ahora sí podemos aplicar la regla del \texttt{FOR}, que nos lleva a tener que probar la siguiente terna:\

$\{ x \leq 2 \wedge x < 2\}$ \texttt{y := y + x} $\{ x \leq 2 \}$, que de forma simplificada nos queda:\\ 

$\{ x < 2\}$ \texttt{y := y + x} $\{ x \leq 2 \}$, sabiendo que $x < 2  \rightarrow x \leq 2$, aplicamos la regla para la postcondición, que nos lleva a tener que probar lo siguiente:\\


$\{ x < 2\}$ \texttt{y := y + x} $\{ x < 2 \}$
, que sabemos se cumple por la regla de la asignación.

\clearpage

\section{Prueba de corrección del algoritmo Mini-AES}
\label{sec:correccion}
En esta sección presentamos la prueba formal de corrección del algoritmo Mini-AES. Probamos que para todo bloque de texto plano (representado por una matriz) y para toda clave, si encriptamos el texto y luego desencriptamos el resultado, el bloque no cambia.

Realizamos la prueba de manera composicional utilizando la lógica de Hoare. Para esto creamos un lema para cada uno de los pasos del algoritmo (KeyAddition, NibbleSub, ShifRow, MixColumns), que luego utilizamos en la prueba principal.

Utilizamos la siguiente notación: escribimos los enunciados de los lemas de corrección con anotaciones indicando las pre y las postcondiciones de cada lema. A las pruebas de los lemas las escribimos con anotaciones luego de cada línea de código, indicando los nuevos valores de las variables que cambiaron de valor. En algunos casos, para que la prueba no sea tan compleja mostramos solo los valores de las variables que cambiaron de valor y omitimos todo lo que permanece invariante; esto es aclarado en cada caso en particular. Donde no tenemos que hacer referencia a ninguna precondición en particular las llamamos \texttt{\{pre\}}. Muchas de estas precondiciones son invariantes que se pasan de un lema a otro para usar en uno en particular. Hablaremos más de esto en la sección correspondiente a las invariantes de este capítulo. A la variable de tipo matriz que representa el bloque de texto la llamamos \texttt{mid}. Denotamos con \texttt{mid\_pre} al valor de dicha variable en las precondiciones de cierto lema. Llamamos \texttt{kid} a una variable que representa una clave y \texttt{kid0}, \texttt{kid1} y \texttt{kid2} a cada una de las claves generadas para cada una de las rondas del algoritmo.

A continuación presentamos una descripción de las invariantes. Luego presentaremos primero la prueba final  y después los lemas auxiliares que se usan. En todos los casos, para pasar de una línea de código a otra, ya sea en los lemas auxiliares o en la prueba final, se utiliza la regla de Hoare para la secuencia; por lo tanto la omitiremos en las demostraciones.

\subsection{Invariantes}
La prueba principal \texttt{hoare\_miniaes} está hecha de manera composicional, dividida en varios lemas: \texttt{hoare\_key\_addition}, \texttt{hoare\_shift\_row}, etc. La forma que tenemos de componer estos lemas es utilizando la regla de Hoare para la secuencia. Esta regla nos dice que las precondiciones de la segunda instrucción deben ser postcondiciones de la primera. Para esto nos definimos un conjunto de invariantes, que son un conjunto de predicados o afirmaciones que son pre y postcondiciones de la prueba principal y de cada uno de los lemas antes mencionados. Cada una de estas invariantes se utiliza en uno o más de los lemas.

\begin{itemize}
    \item La matriz S-box está bien definida; en cada una de sus 16 posiciones tiene el valor correcto.
    \item La matriz S-box inversa está bien definida; en cada una de sus 16 posiciones tiene el valor correcto.
    \item La matriz de multiplicación está bien definida; en cada una de sus 256 posiciones tiene el valor correcto.
    \item Cada una de las matrices que representan la claves de cada ronda están bien definidas; en cada una de sus posiciones tienen valores entre 0 y 15.
    \item El bloque de texto está bien definido; en cada una de sus posiciones tiene valores entre 0 y 15.
\end{itemize}

\subsection{Prueba del lema hoare\_miniaes}
Cuando decimos que vamos a probar la corrección del algoritmo Mini-AES, lo que vamos a probar realmente es que los procedimientos \texttt{encrypt} y \texttt{decrypt} son inversos, es decir, si aplicamos \texttt{encrypt} y luego \texttt{decrypt} sobre un bloque cualquiera, este bloque no cambia. Dicho de otra forma: que los valores de la matriz que representa el bloque son los mismos antes y después de aplicar los dos procedimientos. Sabiendo que \texttt{mid} es la variable donde se almacena el bloque, nuestra prueba consiste en probar la siguiente terna de Hoare:

\begin{lstlisting}[mathescape]
Theorem hoare_miniaes:
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
encrypt mid;
decrypt mid;
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
\end{lstlisting}

Hay varios enfoques que se pueden utilizar para demostrar esto. El más directo sería utilizar las reglas de Hoare básicas (asignación, secuencia, etc.) directamente. Es decir, extender la definición de \texttt{encrypt} y \texttt{decrypt} y luego extender la definición de cada uno de los procedimientos que estos contienen (MixColumns, ShiftRow, KeyAdditon y NibbleSub) para luego aplicar la correspondiente regla de Hoare. Este enfoque nos llevaría a una prueba muy larga y poco estructurada, donde serían repetidas muchas pruebas que en realidad son análogas. Por lo tanto, vemos necesario dividir este problema en subproblemas más pequeños.

Otro enfoque sería partir cada terna en dos y crear lemas para cada una de estas partes y luego probar el lema utilizando estos dos sublemas y la regla de Hoare para la secuencia. Por ejemplo, un lema para \texttt{encrypt} y para \texttt{decrypt} y así sucesivamente. Este otro enfoque nos llevaría a tener que crear demasiados lemas auxiliares.

Nuestra prueba toma un enfoque intermedio y bastante intuitivo, donde creamos un lema de Hoare para cada uno de los pasos del algoritmo (MixColumns, ShiftRow, KeyAdditon y NibbleSub) y en algunos casos algún otro lema auxiliar. Por lo tanto, lo primero que haremos es extender la definición de \texttt{encrypt} y de \texttt{decrypt}, es decir sustituirlos por sus correspondientes definiciones, lo que nos deja el teorema de la siguiente forma:

\begin{lstlisting}[mathescape]
Theorem hoare_miniaes:
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
key_addition mid kid2;
nibble_sub mid mini_sbox;
shift_row mid;
mix_columns mid mult_table;
key_addition mid kid1;
nibble_sub mid mini_sbox;
shift_row mid;
key_addition mid kid0;
key_addition mid kid0;
shift_row mid;
nibble_sub mid mini_sbox_inv;
key_addition mid kid1;
mix_columns mid mult_table;
shift_row mid;
nibble_sub mid mini_sbox_inv;
key_addition mid kid2;
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
\end{lstlisting}

Ahora nuestra terna de Hoare consta de una secuencia de llamadas a procedimientos que, como dijimos anteriormente, la demostramos utilizando la regla de Hoare para la secuencia, además de una regla de Hoare para cada componente del algoritmo. También utilizamos la regla de Hoare para la consecuencia para poder debilitar las precondiciones. Comenzamos la prueba aplicando la regla de la secuencia, que nos lleva a tener que probar las siguientes dos ternas:

\begin{lstlisting}[mathescape]
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
key_addition mid kid2;
{Q}
\end{lstlisting}

\begin{lstlisting}[mathescape]
{Q}
nibble_sub mid mini_sbox;
shift_row mid;
mix_columns mid mult_table;
key_addition mid kid1;
nibble_sub mid mini_sbox;
shift_row mid;
key_addition mid kid0;
key_addition mid kid0;
shift_row mid;
nibble_sub mid mini_sbox_inv;
key_addition mid kid1;
mix_columns mid mult_table;
shift_row mid;
nibble_sub mid mini_sbox_inv;
key_addition mid kid2;
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
\end{lstlisting}

Ahora, para la primera terna podemos aplicar nuestro lema definido en \ref{subsec:lema_keyaddition}, \texttt{hoare\_key\_addition}, que nos instancia la variable \texttt{Q} en la segunda terna y nos lleva a tener que demostrar lo siguiente:

\begin{lstlisting}[mathescape]
{$mid = \left( \begin{array}{cc}m00 \oplus kid2\_00 & m01 \oplus kid2\_01 \\ m10 \oplus kid2\_10 & m11 \oplus kid2\_11)\end{array} \right)$}
nibble_sub mid mini_sbox;
shift_row mid;
mix_columns mid mult_table;
key_addition mid kid1;
nibble_sub mid mini_sbox;
shift_row mid;
key_addition mid kid0;
key_addition mid kid0;
shift_row mid;
nibble_sub mid mini_sbox_inv;
key_addition mid kid1;
mix_columns mid mult_table;
shift_row mid;
nibble_sub mid mini_sbox_inv;
key_addition mid kid2;
{$mid = \left( \begin{array}{cc}m00 & m01\\ m10 & m11\end{array} \right)$}
\end{lstlisting}

Procedemos de la misma forma con el resto de las instrucciones; aplicamos la regla de la secuencia, la regla de la consecuencia para poder relajar las precondiciones en el caso que corresponda y luego el correspondiente lema para cada procedimiento.

Pero esto no es todo, a medida que vamos aplicando las reglas para cada uno de los pasos, el valor de cada una de las posiciones de la matriz \texttt{mid} va cambiando. Antes de empezar, el valor de la posición [0][0] de \texttt{mid} es \texttt{m00}, luego de aplicar \texttt{key\_addition mid kid2} el valor de la posición [0][0] es \texttt{m00 $\oplus$ kid2\_00}, luego aplicamos \texttt{nibble\_sub mid miniSboxId} y el valor de [0][0] pasa a ser sbox[0][m00 $\oplus$ kid2\_00], y así sucesivamente con cada uno de los pasos del algoritmo y para cada posición de la matriz. Vemos de esta forma que al llegar al final, lo que nos queda en la posición [0][0] de \texttt{mid} es equivalente a \texttt{m00}, pero no es sintácticamente igual. Para poder reducir esta expresión y terminar la prueba, necesitamos lemas que prueben que la función \texttt{xor} es inversa de sí misma, que la S-box y su inversa son efectivamente inversas, y que la tabla de multiplicación es inversa de sí misma. La prueba completa, con mayor, detalle se encuentra en el anexo \ref{anexo:prueba}.

\subsection{Prueba del lema hoare\_key\_addition}
\label{subsec:lema_keyaddition}

\begin{lstlisting}[mathescape]
Lema hoare_key_addition:

{pre}
key_addition mid kid
{$\forall$ i,j $\in$ {0,1} : mid[i][j] = mid_pre[i][j] $\oplus$ kid[i][j]}
\end{lstlisting}

Extendemos la definición de \texttt{key\_addition} y escribimos el código con anotaciones:

\begin{lstlisting}[mathescape]
{pre}
mid[0][0] ::= mid_pre[0][0] xor  kid[0][0]
{mid[0][0] = mid_pre[0][0] $\oplus$  kid[0][0]}    (1)
mid[0][1] ::= mid_pre[0][1] xor  kid[0][1]
{mid[0][0] = mid_pre[0][0] $\oplus$  kid[0][0] $\wedge$
 mid[0][1] = mid_pre[0][1] $\oplus$  kid[0][1]}    (2)
mid[1][0] ::= mid_pre[1][0] xor  kid[1][0]
{mid[0][0] = mid_pre[0][0] $\oplus$  kid[0][0] $\wedge$
 mid[0][1] = mid_pre[0][1] $\oplus$  kid[0][1] $\wedge$
 mid[1][0] = mid_pre[1][0] $\oplus$  kid[1][0]}    (3)
mid[1][1] ::= mid_pre[1][1] xor  kid[1][1]
{mid[0][0] = mid_pre[0][0] $\oplus$  kid[0][0] $\wedge$
 mid[0][1] = mid_pre[0][1] $\oplus$  kid[0][1] $\wedge$
 mid[1][0] = mid_pre[1][0] $\oplus$  kid[1][0] $\wedge$
 mid[1][1] = mid_pre[1][1] $\oplus$  kid[1][1]}    (4)
\end{lstlisting}

En los casos (1) (2) (3) y (4) aplicamos la regla de Hoare para la asignación de una posición de la matriz. Vemos que al final se cumple la postcondición del lema.
 
\subsection{Prueba del lema hoare\_shift\_row}
\begin{lstlisting}[mathescape]
Lema hoare_shift_row:

{pre}
shift_row mid
{mid[1][0] = mid_pre[1][1] $\wedge$ mid[1][1] = mid_pre[1][0]}
\end{lstlisting}

Extendemos la definición de \texttt{shift\_row} y escribimos el código con anotaciones:

\begin{lstlisting}[mathescape]
{pre}
byte aux ::= mid_pre[1][0]
{aux = mid_pre[1][0]}		(1)
mid[1][0] ::= mid_pre[1][1]
{aux = mid_pre[1][0] $\wedge$ mid[1][0] = mid_pre[1][1]}	(2)
mid[1][1] ::= aux
{mid[1][0] = mid_pre[1][1] $\wedge$ mid[1][1] = mid_pre[1][0]}    	(3)

\end{lstlisting}

En el paso (1) aplicamos la regla de asignación de Hoare. En los pasos (2) y (3) aplicamos la regla de Hoare para la asignación de una posición de la matriz.

\subsection{Prueba del lema hoare\_nibble\_sub}
\begin{lstlisting}[mathescape]
Lema hoare_nibble_sub:

{pre}
nibble_sub mid sbox
{$\forall$ i,j $\in$ {0,1} : mid[i][j] = sbox[0][mid_pre[i][j]]}

\end{lstlisting}

Extendemos la definición de \texttt{nibble\_sub} y escribimos el código con anotaciones:

\begin{lstlisting}[mathescape]
{pre}
byte a00 ::= mid_pre[0][0]
{a00 = mid_pre[0][0]}			(1)
byte b00 ::= sbox[0][a00]
{b00 = sbox[0][mid_pre[0][0]]}		(2)
mid[0][0] ::= b00
{mid[0][0] = sbox[0][mid_pre[0][0]]}	(3)

byte a01 ::= mid_pre[0][1]
{a01 = mid_pre[0][1]}			(4)
byte b01 ::= sbox[0][a01]
{b01 = sbox[0][mid_pre[0][1]]}		(5)
mid[0][1] ::= b01
{mid[0][1] =sbox[0][mid_pre[0][1]]}	(6)

byte a10 ::= mid_pre[1][0]
{a10 = mid_pre[1][0]}			(7)
byte b10 ::= sbox[0][a10]
{b10 = sbox[0][mid_pre[1][0]]}		(8)
mid[1][0] ::= b10
{mid[1][0] =sbox[0][mid_pre[1][0]]}	(9)

byte a11 ::= mid_pre[1][1]
{a11 = mid_pre[1][1]}			(10)
byte b11 ::= sbox[0][a11]
{b11 = sbox[0][mid_pre[1][1]]}		(11)
mid[1][1] ::= b11
{mid[1][1] =sbox[0][mid_pre[1][1]]}	(12)
\end{lstlisting}

En los pasos (1), (2), (4), (5), (7), (8), (10) y (11) aplicamos la regla de Hoare para la asignación a una variable. En los pasos (3), (6), (9) y (12) aplicamos la regla de Hoare para la asignación de una posición de la matriz. En todos los pasos omitimos anotar las variables y posiciones de la matriz que no cambian de valor, para que la prueba no que la prueba no sea muy compleja.

\subsection{Prueba del lema hoare\_mix\_columns}
\begin{lstlisting}[mathescape]
Lema hoare_mix_columns:

{pre}
mix_columns mid sbox
{$\forall$ i,j $\in$ {0,1} : mid[i][j] = mult_table[mid_pre[i][j]][mid_pre[$\lnot$i][j]]}

\end{lstlisting}

Extendemos la definición de \texttt{mix\_columns} y escribimos el código con anotaciones:

\begin{lstlisting}[mathescape]
{pre}
byte a00 ::= mid[0][0]
{a00 = mid_pre[0][0]}					(1)
byte a10 ::= mid[1][0]
{a10 = mid_pre[1][0]}					(2)

mid[0][0] ::= (mult_table[a00][a10])
{mid[0][0] = mult_table[mid_pre[0][0]][mid_pre[1][0]]} 	(3)
mid[1][0] ::= (mult_table[a10][a00])
{mid[1][0] = mult_table[mid_pre[1][0]][mid_pre[0][0]]}	(4)

byte a01 ::= mid[0][1]
{a01 = mid_pre[0][1]}					(5)
byte a11 ::= mid[1][1]
{a11 = mid_pre[1][1]}					(6)

mid[0][1] ::= (mult_table[a01][a11])
{mid[0][1] = mult_table[mid_pre[0][1]][mid_pre[1][1]]} 	(7)
mid[1][1] ::= (mult_table[a11][a01])
{mid[1][1] = mult_table[mid_pre[1][1]][mid_pre[0][1]]} 	(8)
\end{lstlisting}

En los casos (1) (2) (5) y (6) aplicamos la regla de Hoare para la asignación, y en los pasos (3) (4) (7) y (8) aplicamos la regla de Hoare para la asignación de una posición de la matriz. Como las posiciones que no cambian las omitimos en cada paso, vemos que al final se cumple la postcondición del lema.

\subsection{Lemas auxiliares}
En esta sección describimos algunos de los lemas auxiliares que se usan tanto en la prueba principal así como en los lemas que usa esta prueba.

\subsubsection*{mini\_sbox\_result}
Este lema nos dice que la S-box está compuesta por nibbles, es decir que en todas sus posiciones contiene bytes entre 0 y 15:
\begin{lstlisting}[mathescape]
Lema mini_sbox_result:

$\forall$ x,y : 0<=x<16 $\rightarrow$ miniSbox[0][x] = y $\rightarrow$ 0<=y<16.
\end{lstlisting}

\subsubsection*{mini\_sbox\_inv\_result}
Este lema nos dice que la S-box inversa está compuesta por nibbles, es decir que en todas sus posiciones contiene bytes entre 0 y 15:
\begin{lstlisting}[mathescape]
Lema mini_sbox_inv_result:

$\forall$ x,y : 0<=x<16 $\rightarrow$ miniSboxInv[0][x] = y $\rightarrow$ 0<=y<16.
\end{lstlisting}

\subsubsection*{miniSboxInv}
Este lema nos dice que la S-box y la S-box inversa son efectivamete inversas:
\begin{lstlisting}[mathescape]
Lema miniSboxInv:

$\forall$ x,y : 0<=x<16 $\rightarrow$ miniSbox[0][x] = y $\rightarrow$ miniSboxInv[0][y] = x
\end{lstlisting}

\subsubsection*{mult\_table\_inv}
Este lema nos dice que la tabla de multiplicación es inversa de sí misma:
\begin{lstlisting}[mathescape]
Lema mult_table_inv:

$\forall$ x1, x2, x3, x4 : 0<=x1<16 $\rightarrow$ 0<=x2<16 $\rightarrow$ mult_table[x1][x2] = x3 $\rightarrow$ 
mult_table[x2][x1] = x4 $\rightarrow$ (mult_table[x3][x4] = x1 $\wedge$ mult_table[x4][x2] = x2)
\end{lstlisting}

\subsubsection*{mult\_table\_result}
Este lema nos dice que la tabla de multiplicación está compuesta por nibbles, es decir que en todas sus posiciones contiene bytes entre 0 y 15:
\begin{lstlisting}[mathescape]
Lema mult_table_result:

$\forall$ x,y : 0<=x<16 $\rightarrow$  0<=y<16 $\rightarrow$ mult_table[x][y] = b $\rightarrow$ 0<=b<16.
\end{lstlisting}


\subsubsection*{nibble\_xor}
Este lema nos dice que el xor de dos bytes menores que 16 es menor que 16:
\begin{lstlisting}[mathescape]
Lema nibble_xor:

$\forall$ x, y : 0<=x<16 $\rightarrow$ 0<=y<16 $\rightarrow$ (x xor y) < 16
\end{lstlisting}


\clearpage

\section{Conclusiones y trabajo a futuro}
\label{sec:conclusiones}
En este trabajo se presentó el diseño de un lenguaje de programación imperativo, que permite implementar algoritmos criptográficos. El lenguaje cuenta con los tipos primitivos:  entero, byte, booleano y matrices de bytes, asi como declaración de variables e instrucciones de asignación, loops y condicionales. Sobre este lenguaje fueron implementados AES y Mini-AES. Por último fue realizada con éxito la prueba de corrección de Mini-AES, utilizando la lógica de Hoare. Esta prueba garantiza que la implementación brindada funciona correctamente: al encriptar un texto plano y desencriptar el resultado se obtiene el texto original.

Este trabajo resulta relevante en cuanto a la criticidad de los temas tratados. El algoritmo AES es sumamente utilizado a nivel internacional y por organizaciones que operan con información sensible de usuarios en todo el mundo. Por ello consideramos importante contar con implementaciones certificadas, es decir, que junto con ellas se presente una prueba formal de su correcto funcionamiento. Se aprovechó el aporte de Mini-AES, que si bien no es utilizado en la práctica, sirve como primer paso hacia la especificación y verificación de AES. Debido a que no fueron encontradas pruebas formales para las implementaciones actuales ni resultados análogos al presente, consideramos a éste como un primer acercamiento al tema.

Se plantea que este trabajo sirva como base para realizar más pruebas, que verifiquen la seguridad de la implementación presentada de Mini-AES. Por ejemplo, se puede probar el correcto manejo de memoria, de forma de no revelar ningún tipo de información sensible \cite{cache}. Para esto, es necesario implementar las primitivas de acceso a memoria del lenguaje aquí diseñado en una plataforma ---como la considerada en \cite{virtualcert}, por ejemplo--- que permita ejecutar las instrucciones.

También se propone realizar las mismas pruebas sobre la implementación de AES aquí presentada. Éstas pueden resultar más complejas debido a la propia complejidad del algoritmo. AES, a diferencia de Mini-AES, contiene sentencias condicionales y loops, además de utilizar bytes completos en lugar de nibbles. Sin embargo, en este trabajo se brinda un marco de trabajo. Contando con la prueba de Mini-AES aquí desarrollada, se puede seguir un enfoque muy similar de prueba, dividiendo en lemas por operaciones y probando dichos lemas por separado. Además de ello se desarrolló un conjunto de lemas útiles para utilizar la lógica de Hoare, que pueden ser reutilizados. Incluso es posible realizar el mismo conjunto de pruebas sobre algoritmos criptográficos de clave pública, como RSA \cite{rsa}.

Otro posible trabajo a futuro puede tratarse de extender al lenguaje aquí presentado. Por ejemplo agregar tipos primitivos ---entre otros, caracteres y cadenas de caracteres--- y procedimientos con retorno de valores. Esto permitiría que el lenguaje sea más similar a los lenguajes con los que usualmente se implementan los algoritmos criptográficos, permitiendo generar implementaciones de referencia más realistas y fáciles de traducir a otros lenguajes. Además ello simplificaría la implementación de nuevos algoritmos, que pueden ser más complejos y requerir las herramientas mencionadas.

\clearpage

\nocite{*}
\bibliography{Informe}
\bibliographystyle{plain}


\clearpage

\appendix
\section{Lenguaje completo}
\label{anexo:lenguaje}
En este apéndice se presenta la definición completa del lenguaje diseñado. El código presentado es prácticamente igual al código Coq original, a excepción de algunas palabras claves y símbolos de puntuación. Estos fueron quitados para lograr un código más sencillo de leer.

\subsection{Sintaxis}
\label{subsec:apendice_sintaxis}
En esta subsección se presentan solamente las definiciones mediante las cuales se pueden construir expresiones e instrucciones válidas del lenguaje.

\subsubsection{Expresiones}
Utilizando los tipos aquí presentados se construyen las expresiones aritméticas, booleanas, de bytes o de matrices. Se definen de forma recursiva pudiendo ser combinadas para generar expresiones complejas.

\begin{lstlisting}
Id := id :
  nat -> Id

ArithExp := 
  arith_exp_num   : Integer  -> ArithExp
  arith_exp_id    : Id       -> ArithExp
  arith_exp_plus  : ArithExp -> ArithExp -> ArithExp
  arith_exp_minus : ArithExp -> ArithExp -> ArithExp
  arith_exp_mult  : ArithExp -> ArithExp -> ArithExp
  arith_exp_div   : ArithExp -> ArithExp -> ArithExp
  arith_exp_mod   : ArithExp -> ArithExp -> ArithExp

BoolExp := 
  bool_exp_lit : Bool     -> BoolExp
  bool_exp_id  : Id       -> BoolExp
  bool_exp_not : BoolExp  -> BoolExp
  bool_exp_eq  : ArithExp -> ArithExp -> BoolExp
  bool_exp_lt  : ArithExp -> ArithExp -> BoolExp
  bool_exp_le  : ArithExp -> ArithExp -> BoolExp
  bool_exp_gt  : ArithExp -> ArithExp -> BoolExp
  bool_exp_gtb : ByteExp  -> ByteExp  -> BoolExp
  bool_exp_eqb : ByteExp  -> ByteExp  -> BoolExp
  bool_exp_ge  : ArithExp -> ArithExp -> BoolExp
  bool_exp_and : BoolExp  -> BoolExp  -> BoolExp
  bool_exp_or  : BoolExp  -> BoolExp  -> BoolExp

ByteExp :=
  byte_exp_num    : Byte      -> ByteExp
  byte_exp_id     : Id        -> ByteExp
  byte_exp_xor    : ByteExp   -> ByteExp  -> ByteExp
  byte_exp_andbb  : ByteExp   -> ByteExp  -> ByteExp
  byte_exp_shiftl : ByteExp   -> ArithExp -> ByteExp
  byte_exp_shiftr : ByteExp   -> ArithExp -> ByteExp
  byte_exp_matrix : MatrixExp -> ArithExp -> ArithExp -> ByteExp

MatrixExp :=
  matrix_exp_init : ArithExp -> ArithExp -> MatrixExp
  matrix_exp_lit  : forall A m n, Matrix A m n -> MatrixExp
  matrix_exp_id   : Id -> MatrixExp
\end{lstlisting}

\subsubsection{Instrucciones}
\label{subsec:apendice_instrucciones}
Las instrucciones son ejecutadas una a una al ser evaluadas. Estas son las que, al ser evaluadas, realizan cambios de estado.

\begin{lstlisting}[mathescape]
Instr :=
  instr_skip          : Instr
  instr_assign_bool   : Id      $\rightarrow$ BoolExp    $\rightarrow$ Instr
  instr_assign_int    : Id      $\rightarrow$ ArithExp   $\rightarrow$ Instr
  instr_assign_byte   : Id      $\rightarrow$ ByteExp    $\rightarrow$ Instr
  instr_assign_matrix : Id      $\rightarrow$ MatrixExp $\rightarrow$ Instr
  instr_seq           : Instr   $\rightarrow$ Instr      $\rightarrow$ Instr
  instr_if            : BoolExp $\rightarrow$ Instr      $\rightarrow$ Instr     $\rightarrow$ Instr
  instr_while         : BoolExp $\rightarrow$ Instr      $\rightarrow$ Instr
  instr_for           : Id      $\rightarrow$ ArithExp   $\rightarrow$ Instr     $\rightarrow$ Instr
  instr_matrix_set    : Id      $\rightarrow$ ArithExp   $\rightarrow$ ArithExp $\rightarrow$ ByteExp $\rightarrow$ Instr
\end{lstlisting}

\subsubsection*{Notación}
Esta notación puede ser utilizada al escribir programas en el lenguaje presentado. En la columna \textit{Constructor} se muestra la notación utilizando directamente el constructor de Coq, en \textit{Símbolo} se muestra su contraparte con notación simplificada. Notar que en muchos casos la notación es infija, es decir que el símbolo se coloca entre los operandos.

\begin{table}[ht]
	\centering
	\begin{tabular}{|c|c|}
		\hline
		\textbf{Constructor} & \textbf{Símbolo} \\ \hline
		arith\_exp\_num a & a \\ \hline
		arith\_exp\_id a & a \\ \hline
		arith\_exp\_plus a b & a \texttt{+} b \\ \hline
		arith\_exp\_minus a b & a \texttt{-} b \\ \hline
		arith\_exp\_mult a b & a \texttt{*} b \\ \hline
		arith\_exp\_div a b & a \texttt{/} b \\ \hline
		arith\_exp\_mod a b & a \texttt{\%} b \\
		\hline
	\end{tabular}
	\caption{Notación para expresiones aritméticas.}
	\label{notacion:arith_exp}
\end{table}

\begin{table}[ht]
	\centering
	\begin{tabular}{|c|c|}
		%\hline
		\textbf{Constructor} & \textbf{Símbolo} \\ \hline
		bool\_exp\_lit a & a \\ \hline
		bool\_exp\_id a & a \\ \hline
		bool\_exp\_eq a b & a \texttt{==} b \\ \hline
		bool\_exp\_lt a b & a \texttt{lt} b \\ \hline
		bool\_exp\_le a b & a \texttt{le} b \\ \hline
		bool\_exp\_gt a b & a \texttt{gt} b \\ \hline
		bool\_exp\_ge a b & a \texttt{ge} b \\ \hline
		bool\_exp\_not a & \texttt{!a} \\ \hline
		bool\_exp\_and a b & a \texttt{\&\&} b \\ \hline
		bool\_exp\_or a b & a \texttt{||} b \\ \hline
	\end{tabular}
	\caption{Notación para expresiones booleanas.}
	\label{notacion:bool_exp}
\end{table}

\begin{table}[ht]
	\centering
	\begin{tabular}{|c|c|}
		\hline
		\textbf{Constructor} & \textbf{Símbolo} \\ \hline
		byte\_exp\_num a & a \\ \hline
		byte\_exp\_id a & a \\ \hline
		byte\_exp\_xor a b & a \texttt{xor} b \\ \hline
		byte\_exp\_andbb a b & a \texttt{and} b \\ \hline
		byte\_exp\_shiftl a b & a \texttt{shl} b \\ \hline
		byte\_exp\_shiftr a b & a \texttt{shr} b \\ \hline
		byte\_exp\_matrix matr i j & \texttt{matr[i][j]} \\
		\hline
	\end{tabular}
	\caption{Notación para expresiones de bytes.}
	\label{notacion:byte_exp}
\end{table}

\subsection{Semántica}
\label{subsec:apendice_semantica}
A continuación se presenta la definición formal completa de la evaluación del lenguaje. Al evaluar las expresiones e instrucciones del lenguaje estamos dándole semántica, esto es, estamos definiendo el resultado de ejecutar el programa.

\subsubsection{Expresiones}
La evaluación de una expresión siempre se puede ver como un resultado de una operación, que puede implicar leer un valor de la memoria, pero que no realiza cambios en la misma.

\begin{lstlisting}[mathescape, caption=Relación que define la evaluación de expresiones aritméticas.]
ArithEval :=
  arith_eval_num   : $\forall$ (n: Integer),
      arith_exp_num n $\Downarrow$ n

  arith_eval_id    : $\forall$ (i: Id)(z: Integer),
      st i = Some (int_val z) $\rightarrow$ arith_exp_id i $\Downarrow$  z

  arith_eval_plus  : $\forall$ (e1 e2: ArithExp) (n1 n2: Integer), 
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 + e2 $\Downarrow$ int_plus n1 n2 

  arith_eval_minus : $\forall$ (e1 e2: ArithExp) (n1 n2: Integer), 
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 - e2 $\Downarrow$ int_minus n1 n2

  arith_eval_mult  : $\forall$ (e1 e2: ArithExp) (n1 n2: Integer), 
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 * e2 $\Downarrow$ int_mult n1 n2

  arith_eval_div   : $\forall$ (e1 e2: ArithExp) (n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 / e2 $\Downarrow$ int_div n1 n2

  arith_eval_mod   : $\forall$ (e1 e2: ArithExp) (n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 % e2 $\Downarrow$ int_modulo n1 n2
\end{lstlisting}
\begin{lstlisting}[mathescape, caption=Relación que define la evaluación de expresiones booleanas.]
BoolEval :=
  bool_eval_lit : $\forall$ (b: Bool),
      bool_exp_lit b $\Downarrow$ b

  bool_eval_id  : $\forall$ (i:Id)(b:Bool),
       st i = Some (bool_val b) $\rightarrow$ (bool_exp_id i) $\Downarrow$ b

  bool_eval_eq  : $\forall$ (e1 e2: ArithExp)(n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 == e2 $\Downarrow$ int_eq n1 n2
 
 bool_eval_eqb  : $\forall$ (e1 e2: ByteExp)(n1 n2: Byte),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 == e2 $\Downarrow$ byte_eq n1 n2

  bool_eval_lt  : $\forall$ (e1 e2: ArithExp)(n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 < e2 $\Downarrow$ int_lt n1 n2

  bool_eval_le  : $\forall$ (e1 e2: ArithExp)(n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 $\leq$ e2 $\Downarrow$ int_le n1 n2

  bool_eval_gt  : $\forall$ (e1 e2: ArithExp)(n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 > e2 $\Downarrow$ int_gt n1 n2

 bool_eval_gtb  : $\forall$ (e1 e2: ByteExp)(n1 n2: Byte),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 > e2 $\Downarrow$ byte_gt n1 n2

  bool_eval_ge  : $\forall$ (e1 e2: ArithExp)(n1 n2: Integer),
      e1 $\Downarrow$ n1 $\rightarrow$ e2 $\Downarrow$ n2 $\rightarrow$ e1 $\geq$ e2 $\Downarrow$ int_ge n1 n2

  bool_eval_not : $\forall$ (e1: BoolExp)(b1: Bool),
      e1 $\Downarrow$ b1 $\rightarrow$ bool_exp_not e1 $\Downarrow$ $\lnot$b1

  bool_eval_and : $\forall$ (e1 e2: BoolExp)(b1 b2: Bool),
      e1 $\Downarrow$ b1 $\rightarrow$ e2 $\Downarrow$ b2 $\rightarrow$ e1 $\land$ e2 $\Downarrow$ bool_and b1 b2

  bool_eval_or  : $\forall$ (e1 e2: BoolExp)(b1 b2: Bool),
      e1 $\Downarrow$ b1 $\rightarrow$ e2 $\Downarrow$ b2 $\rightarrow$ e1 $\lor$ e2 $\Downarrow$ bool_or b1 b2
\end{lstlisting}
\begin{lstlisting}[mathescape, caption=Relación que define la evaluación de expresiones de bytes.]
ByteEval :=
  byte_eval_lit : $\forall$ (b:Byte),
      byte_exp_num b $\Downarrow$ b

  byte_eval_id : $\forall$ (i:Id)(b:Byte),
      st i = Some (byte_val b) $\rightarrow$ byte_exp_id i $\Downarrow$ b

  byte_eval_xor : $\forall$ (e1 e2: ByteExp)(b1 b2: Byte),
      e1 $\Downarrow$ b1 $\rightarrow$ e2 $\Downarrow$ b2 $\rightarrow$ e1 xor e2 $\Downarrow$ byte_xor b1 b2

  byte_eval_andbb : $\forall$ (e1 e2: ByteExp)(b1 b2: Byte),
      e1 $\Downarrow$ b1 $\rightarrow$ e2 $\Downarrow$ b2 $\rightarrow$ e1 and e2 $\Downarrow$ byte_and b1 b2

  byte_eval_shiftl : $\forall$ (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      e $\Downarrow$ b $\rightarrow$ n $\Downarrow$ x $\rightarrow$ e shl n $\Downarrow$ byte_shl b x

  byte_eval_shiftr : $\forall$ (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      e $\Downarrow$ b $\rightarrow$ n $\Downarrow$ x $\rightarrow$ e shr n $\Downarrow$ byte_shr b x

  byte_eval_matrix :
      $\forall$ (e1 e2: ArithExp) (m n i j: Integer)
        (mexp: MatrixExp) (matr: Matrix Byte m n),
     mexp $\Downarrow$ matr $\rightarrow$ e1 $\Downarrow$ i $\rightarrow$ e2 $\Downarrow$ j $\rightarrow$ mexp[e1][e2] $\Downarrow$ matrix_get i j matr
\end{lstlisting}
\begin{lstlisting}[mathescape, caption=Relación que define la evaluación de expresiones de matrices.]
MatrixEval :=
  matrix_eval_lit : $\forall$ (matr: Matrix Byte m n),
      matrix_exp_lit matr $\Downarrow$ matr
  
  matrix_eval_id : $\forall$ (i: Id)(matr: Matrix Byte m n),
      st i = Some (byte_matrix_val mx) $\rightarrow$ matrix_exp_id i $\Downarrow$ matr

  matrix_eval_init : $\forall$ (e1 e2: ArithExp),
      e1 $\Downarrow$ m $\rightarrow$ e2 $\Downarrow$ n $\rightarrow$ matrix_exp_init e1 e2 $\Downarrow$ matrix_zero m n
\end{lstlisting}

\subsubsection{Instrucciones}
La evaluación de instrucciones, a diferencia de la de expresiones, puede realizar cambios en los valores en memoria. Al cambiar el valor de una variable en memoria decimos que se realiza una transición de un estado a otro. Por esto, la evaluación de instrucciones se define como una relación entre estados.

\begin{lstlisting}[mathescape, caption=Definición inductiva de la evaluación de instrucciones.]
InstrEval :=
  skip_eval :
    instr_skip / st $\Downarrow$ st

  assign_bool_eval : $\forall$ (bid: Id) (bexp: BoolExp) (b: Bool),
    bexp $\Downarrow$ b $\rightarrow$ bool bid ::= bexp / st $\Downarrow$ st[bid $\leftarrow$ b]

  assign_int_eval : $\forall$ (zid: Id) (zexp: ArithExp) (z: Integer),
    zexp $\Downarrow$ z $\rightarrow$ int zid ::= zexp / st $\Downarrow$ st[zid $\leftarrow$ z]

  assign_byte_eval : $\forall$ (bid: Id) (bexp: ByteExp) (b: Byte),
    bexp $\Downarrow$ (Some b) $\rightarrow$ byte bid ::= bexp / st $\Downarrow$ st[bid $\leftarrow$ b]

  assign_matrix_eval : $\forall$ (mid: Id) (m n: Integer)
  		    (matr: Matrix Byte m n) (mexp : MatrixExp),
    mexp $\Downarrow$ matr $\rightarrow$ matrix mid ::= mexp / st $\Downarrow$ st[mid $\leftarrow$ matr]

  seq_eval : $\forall$ (i1 i2: Instr) (st' st'': State),
      i1 / st $\Downarrow$ st' $\rightarrow$ i2 / st' $\Downarrow$ st'' $\rightarrow$ i1 ; i2 / st $\Downarrow$ st''

  if_eval_true : $\forall$ (bexp: BoolExp) (i1 i2 : Instr) (st': State),
      bexp $\Downarrow$ TRUE $\rightarrow$ i1 / st $\Downarrow$ st' $\rightarrow$
      IF bexp THEN i1 ELSE i2 END / st $\Downarrow$ st'

  if_eval_false : $\forall$ (bexp: BoolExp) (i1 i2: Instr) (st': State),
      bexp $\Downarrow$ FALSE $\rightarrow$ i2 / st $\Downarrow$ st' $\rightarrow$
      IF bexp THEN i1 ELSE i2 END / st $\Downarrow$ st'

  while_eval_true : $\forall$ (bexp: BoolExp) (i: Instr) (st' st'': State),
      bexp $\Downarrow$ TRUE $\rightarrow$ i / st $\Downarrow$ st' $\rightarrow$
      WHILE bexp DO i END / st' $\Downarrow$ st'' $\rightarrow$
      WHILE bexp DO i END / st $\Downarrow$ st''

  while_eval_false : $\forall$ (bexp: BoolExp) (i: Instr),
      bexp $\Downarrow$ FALSE $\rightarrow$ WHILE bexp DO i END / st $\Downarrow$ st

  for_eval_end : $\forall$ (i: Id) (n: Integer) (instr: Instr),
      i $\geq$ n $\Downarrow$ TRUE $\rightarrow$ FOR i TO n DO instr END / st $\Downarrow$ st

  for_eval_step : $\forall$ (i: Id) (x n: Integer)
                    (instr: Instr) (st' st'': State),
      i < n $\Downarrow$ TRUE $\rightarrow$ instr / st $\Downarrow$ st' $\rightarrow$ 
      FOR i TO n DO instr END / st' $\Downarrow$ st'' $\rightarrow$
      st' i = Some (int_val x) $\rightarrow$
      st'' i = Some (int _val (x + ONE)) $\rightarrow$
      FOR i TO n DO instr END / st $\Downarrow$ st''

  matrix_set_eval : $\forall$ (m n i j: Integer) (e1 e2: ArithExp) (e: ByteExp)
                      (mid: Id) (matr matr': Matrix Byte m n) (b: Byte),
      mid $\Downarrow$ matr $\rightarrow$ e1 $\Downarrow$ i $\rightarrow$ e2 $\Downarrow$ j $\rightarrow$ e $\Downarrow$ b $\rightarrow$ 
      matrix_set matr i j b = Some matr' $\rightarrow$
      mid[e1][e2] ::= e / st $\Downarrow$ st[mid $\leftarrow$ matr']
\end{lstlisting}

\section{Implementación de AES}
\label{anexo:aes_impl}
Aquí se presenta la implementación completa del estándar AES, implementada sobre el lenguaje anteriormente presentado. Se divide este anexo en una subsección por cada operación que incluye el algoritmo.

\subsection{Key expansion}

\subsubsection*{Sub word}
\begin{lstlisting}
Definition sub_word(w sbox: Id) :=
  int i ::= 1;
  FOR i TO 4 DO
    byte b ::= w[i][1];
    byte row ::= b band 240;(*11110000*)
    byte row ::= row shr 4;
    byte col ::= b band 15;(*00001111*)
    byte aux ::= sbox[row][col];
    w[i][1] ::= aux;
  END
.
\end{lstlisting}

\subsubsection*{Rot word}
\begin{lstlisting}
Definition rot_word(w: Id) :=
  int k ::= 1;
  byte aux ::= w[1][1];
  FOR k TO (Nb -1) DO
    byte sig ::= w[k + 1][1];
    w[k][1] ::= sig;
  END;
  w[4][1] ::= aux;
.
\end{lstlisting}

\subsubsection*{Key expansion}
\begin{lstlisting}
Definition key_expansion(key: Id):=
  int i ::= 1;
  WHILE (i le Nk) DO
    (* w[i] = word(key[4*i], key[4*i+1], key[4*i+2], key[4*i+3]) *)
    byte aux ::= key[1][i];
    w[1][i] ::= aux;

    byte aux ::= key[2][i];
    w[2][i] ::= aux;

    byte aux ::= key[3][i];
    w[3][i] ::= aux;

    byte aux ::= key[4][i];
    w[4][i] ::= aux;

    int i ::= i + 1;
  END;

  int i ::= Nk;
  int auxint ::= Nk * (Nr + 1);

  WHILE (i le auxint) DO
    byte aux ::= w[1][i - 1];
    temp[1][1] ::= aux;
    byte aux ::= w[2][i - 1];
    temp[1][2] ::= aux;
    byte aux ::= w[3][i - 1];
    temp[1][3] ::= aux;
    byte aux ::= w[4][i - 1];
    temp[1][4] ::= aux;

    IFB (i mod Nk == 1) THEN
      rot_word temp;
      sub_word temp sbox;

      byte temp ::= temp xor rcon[1][i / Nk];
    ELSE
      sub_word temp sbox;
    END;

    (* w[i] = w[i-Nk] xor temp *)
    byte aux ::= w[1][i - Nk] xor temp;
    w[i - 1][1] ::= aux;
    byte aux ::= w[2][i - Nk] xor temp;
    w[i - 1][2] ::= aux;
    byte aux ::= w[3][i - Nk] xor temp;
    w[i - 1][3] ::= aux;
    byte aux ::= w[4][i - Nk];
    w[i - 1][4] ::= aux;

    int i ::= i + 1;
  END
.
\end{lstlisting}

\subsection{AES cipher}
\subsubsection*{Sub bytes}
\begin{lstlisting}
Definition sub_bytes(matr: Id)(sbox: Id):=
  int i ::= 1;
  int j ::= 1;

  FOR i TO Nb DO
    FOR j TO 4 DO
      byte b ::= matr[i][j];
      byte row ::= b band 240;(*11110000*)
      byte row ::= row shr 4;
      byte col ::= b band 15;(*00001111*)
      byte aux ::= sbox[row][col];
      matr[i][j] ::= aux;
    END
  END
.
\end{lstlisting}

\subsubsection*{AddRoundKey}
\begin{lstlisting}
Definition add_round_key(matr: Id)(key: Id)(offset: ArithExp) :=
  int i ::= offset + 1;
  int j ::= 1;

  FOR i TO Nb DO
    FOR j TO 4 DO
      byte x ::= matr[i][j];
      byte y ::= key[i][j];
      matr[i][j] ::= x xor y;
    END
  END
.
\end{lstlisting}

\subsubsection*{Galois multiplication 2}
\begin{lstlisting}
(* Galois mult 2 *)
Definition gmul2(b: Id) :=
  byte b ::= b shl 1;
  IFB (b gt 255) THEN
    byte b ::= b xor 27;
  END
.
\end{lstlisting}

\subsubsection*{Galois multiplication 3}
\begin{lstlisting}
(* Galois mult 3 *)
Definition gmul3(b: Id) :=
  byte baux ::= b;
  byte b ::= b shl 1;

  IFB (b gt 255) THEN
    byte b ::= b xor 27;
  END;
  byte b ::= b xor baux;
.
\end{lstlisting}

\subsubsection*{Mix columns}
\begin{lstlisting}
Definition mix_columns(matr: Id) :=
  int i ::= 1;

  FOR i TO Nb DO
    byte a0 ::= matr[i][1];
    byte a1 ::= matr[i][2];
    byte a2 ::= matr[i][3];
    byte a3 ::= matr[i][4];

    byte gmul2a0 ::= a0;
    byte gmul3a0 ::= a0;
    byte gmul2a1 ::= a1;
    byte gmul3a1 ::= a1;
    byte gmul2a2 ::= a2;
    byte gmul3a2 ::= a2;
    byte gmul2a3 ::= a3;
    byte gmul3a3 ::= a3;

    gmul2 gmul2a0;
    gmul3 gmul3a0;
    gmul2 gmul2a1;
    gmul3 gmul3a1;
    gmul2 gmul2a2;
    gmul3 gmul3a2;
    gmul2 gmul2a3;
    gmul3 gmul3a3;

    matr[i][1] ::= gmul2a0 xor gmul3a1 xor a2 xor a3;
    matr[i][2] ::= a0 xor gmul2a1 xor gmul3a2 xor a3;
    matr[i][3] ::= a0 xor a1 xor gmul2a2 xor gmul3a3;
    matr[i][4] ::= gmul3a0 xor a1 xor a2 xor gmul2a3;
  END
.
\end{lstlisting}

\subsubsection*{Shift rows}
\begin{lstlisting}
Definition shift_rows(matr: Id) :=
  int i ::= 1;
  int j ::= 1;

  FOR i TO Nb DO
    FOR j TO i DO
      byte aux ::= matr[1][j];

      FOR k TO 3 DO
        byte sig ::= matr[i + 1][k];
        matr[i][k] ::= sig;
      END;

      matr[i][j] ::= aux;
    END
  END
.  
\end{lstlisting}

\subsubsection*{AES cipher}
\begin{lstlisting}
Definition aes_cipher (state: Id) :=
  add_round_key state w 1;
  int round ::= 1;
  FOR round TO Nr DO
    sub_bytes state sbox;
    shift_rows state;
    mix_columns state;
    add_round_key state w (round * Nb);
  END;

  sub_bytes state sbox;
  shift_rows state;
  add_round_key state w (round * Nb);
.
\end{lstlisting}

\section{Prueba de Mini-AES}
\label{anexo:prueba}
Se presenta a continuación una prueba completa de la relación inversa que existe entre los procedimientos de encriptar y desencriptar. Esta prueba se aleja de la prueba realizada en Coq en el trabajo, ya que no se encuentra escrita en ningún lenguaje formal. Sin embargo, la estructura de la prueba y la lógica utilizada es análoga a la realizada en este trabajo. El código fuente de la prueba formal, verificada en Coq, se encuentra en las referencias de la sección \ref{subsec:codigo}.

Aclaración: nos resulta útil saber el valor de la matriz de estado en un estado del programa; por lo tanto denotamos como \texttt{mid\_i} el valor de dicha variable en el estado \texttt{i} del programa.

\begin{lstlisting}[mathescape]
Lema hoare_miniaes:
{pre}
encrypt mid
decrypt mid
{$\forall$ i,j : mid[i][j] = mid_pre[i][j]}
\end{lstlisting}


Para la prueba de corrección, extendemos la definición de encrypt y de decrypt y nos queda lo siguiente:

\begin{lstlisting}[mathescape]
{pre}
key_addition mid kid2
{mid_1[0][0] = mid_0[0][0] $\oplus$  kid2[0][0] $\wedge$
 mid_1[0][1] = mid_0[0][1] $\oplus$  kid2[0][1] $\wedge$
 mid_1[1][0] = mid_0[1][0] $\oplus$  kid2[1][0] $\wedge$
 mid_1[1][1] = mid_0[1][1] $\oplus$  kid2[1][1]} (s1)
nibble_sub mid miniSboxId
{mid_2[0][0] = sbox[0][mid_1[0][0]] $\wedge$
 mid_2[0][1] = sbox[0][mid_1[0][1]] $\wedge$
 mid_2[1][0] = sbox[0][mid_1[1][0]] $\wedge$
 mid_2[1][1] = sbox[0][mid_1[1][1]]} (s2)
shift_row mid
{mid_3[1][0] = mid_2[1][1] $\wedge$
 mid_3[1][1] = mid_2[1][0]} (s3)
mix_columns mid mult_table
{mid_4[0][0] = mult_table[mid_3[0][0]][mid_3[1][0]] $\wedge$
 mid_4[0][1] = mult_table[mid_3[0][1]][mid_3[1][1]] $\wedge$
 mid_4[1][0] = mult_table[mid_3[1][0]][mid_3[0][0]] $\wedge$
 mid_4[1][1] = mult_table[mid_3[1][1]][mid_3[0][1]]} (s4)
 
key_addition mid kid1
{mid_5[0][0] = mid_4[0][0] $\oplus$  kid1[0][0] $\wedge$
 mid_5[0][1] = mid_4[0][1] $\oplus$  kid1[0][1] $\wedge$
 mid_5[1][0] = mid_4[1][0] $\oplus$  kid1[1][0] $\wedge$
 mid_5[1][1] = mid_4[1][1] $\oplus$  kid1[1][1]} (s5)
shift_row mid
{mid_6[1][0] = mid_5[1][1] $\wedge$
 mid_6[1][1] = mid_5[1][0]} (s6)
nibble_sub mid miniSboxId
{mid_7[0][0] = sbox[0][mid_6[0][0]] $\wedge$
 mid_7[0][1] = sbox[0][mid_6[0][1]] $\wedge$
 mid_7[1][0] = sbox[0][mid_6[1][0]] $\wedge$
 mid_7[1][1] = sbox[0][mid_6[1][1]]} (s7)

key_addition mid kid0
{mid_8[0][0] = mid_7[0][0] $\oplus$  kid0[0][0] $\wedge$
 mid_8[0][1] = mid_7[0][1] $\oplus$  kid0[0][1] $\wedge$
 mid_8[1][0] = mid_7[1][0] $\oplus$  kid0[1][0] $\wedge$
 mid_8[1][1] = mid_7[1][1] $\oplus$  kid0[1][1]} (s8)

key_addition mid kid0
{mid_9[0][0] = mid_8[0][0] $\oplus$  kid0[0][0] $\wedge$
 mid_9[0][1] = mid_8[0][1] $\oplus$  kid0[0][1] $\wedge$
 mid_9[1][0] = mid_8[1][0] $\oplus$  kid0[1][0] $\wedge$
 mid_9[1][1] = mid_8[1][1] $\oplus$  kid0[1][1]} (s9)
 
nibble_sub mid sboxInv
{mid_10[0][0] = sboxInv[0][mid_9[0][0]] $\wedge$
 mid_10[0][1] = sboxInv[0][mid_9[0][1]] $\wedge$
 mid_10[1][0] = sboxInv[0][mid_9[1][0]] $\wedge$
 mid_10[1][1] = sboxInv[0][mid_9[1][1]]} (s10)

shift_row mid
{mid_11[1][0] = mid_10[1][1] $\wedge$
 mid_11[1][1] = mid_10[1][0]} (s11)
 
key_addition mid kid1
{mid_12[0][0] = mid_11[0][0] $\oplus$  kid1[0][0] $\wedge$
 mid_12[0][1] = mid_11[0][1] $\oplus$  kid1[0][1] $\wedge$
 mid_12[1][0] = mid_11[1][0] $\oplus$  kid1[1][0] $\wedge$
 mid_12[1][1] = mid_11[1][1] $\oplus$  kid1[1][1]} (s12)
 
mix_columns mid mult_table
{mid_13[0][0] = mult_table[mid_12[0][0]][mid_12[1][0]] $\wedge$
 mid_13[0][1] = mult_table[mid_12[1][0]][mid_12[0][0]] $\wedge$
 mid_13[1][0] = mult_table[mid_12[0][1]][mid_12[1][1]] $\wedge$
 mid_13[1][1] = mult_table[mid_12[1][1]][mid_12[0][1]]} (s13)
 
shift_row mid
{mid_14[1][0] = mid_13[1][1] $\wedge$
 mid_14[1][1] = mid_13[1][0]} (s14)
 
nibble_sub mid sboxInv
{mid_15[0][0] = sboxInv[0][mid_14[0][0]] $\wedge$
 mid_15[0][1] = sboxInv[0][mid_14[0][1]] $\wedge$
 mid_15[1][0] = sboxInv[0][mid_14[1][0]] $\wedge$
 mid_15[1][1] = sboxInv[0][mid_14[1][1]]} (s15)
(s1) Esto se cumple por el lema hoare_key_addition mid\_0 kid2 \\
(s2) lema hoare_nibble_sub\\
(s3) hoare_shift_row\\
(s4) hoare_mix_columns
key_addition mid kid2
{mid_16[0][0] = mid_15[0][0] $\oplus$  kid2[0][0] $\wedge$
 mid_16[0][1] = mid_15[0][1] $\oplus$  kid2[0][1] $\wedge$
 mid_16[1][0] = mid_15[1][0] $\oplus$  kid2[1][0] $\wedge$
 mid_16[1][1] = mid_15[1][1] $\oplus$  kid2[1][1]} (s16)

\end{lstlisting}

En cada uno de los pasos s1..s16 aplicamos el correspondiente lema, de los lemas anteriormente vistos: key\_addition, nibble\_sub, shift\_row y mix\_columns.\\

Ahora tenemos que probar por que $mid_{16}[i][j]\ =\ mid_0[i][j]\ \forall\ i,j\ \in\ \{0,1\}$

Comenzaremos por sustituir (s8) en (s9) y nos queda lo siguiente:
\begin{equation} \label{eq:s8s9}
\begin{aligned}
mid_9[0][0] &= mid_7[0][0] \oplus kid0[0][0] \oplus  kid0[0][0] \\
            &= mid_7[0][0] \\
mid_9[0][1] &= mid_7[0][1] \oplus kid0[0][1] \oplus  kid0[0][1] \\
            &= mid_7[0][1] \\
mid_9[1][0] &= mid_7[1][0] \oplus kid0[1][0] \oplus  kid0[1][0] \\
            &= mid_7[1][0] \\
mid_9[1][1] &= mid_7[1][1] \oplus kid0[1][1] \oplus  kid0[1][1] \\
            &= mid_7[0][0]
\end{aligned}
\end{equation}

En (s10) sustituyendo con lo obtenido en (\ref{eq:s8s9}) tenemos:
\begin{equation} \label{eq:s10}
\begin{aligned}
mid_10[0][0] = sboxInv[mid_7[0][0]] \\
mid_10[0][1] = sboxInv[mid_7[0][1]] \\
mid_10[1][0] = sboxInv[mid_7[1][0]] \\
mid_10[1][1] = sboxInv[mid_7[1][1]]
\end{aligned}
\end{equation}
Sustituyendo en (\ref{eq:s10}) con las equaciones de (s7) nos queda
\begin{equation*}
\begin{aligned}
mid_10[0][0] = sboxInv[sbox[mid_6[0][0]]] \\
mid_10[0][1] = sboxInv[sbox[mid_6[0][1]]] \\
mid_10[1][0] = sboxInv[sbox[mid_6[1][0]]] \\
mid_10[1][1] = sboxInv[sbox[mid_6[1][1]]]
\end{aligned}
\end{equation*}
Sabiendo que sbox y sboxInv son inversas llegamos a que:
\begin{equation} \label{eq:s12}
\begin{aligned}
mid_{10}[0][0] = mid_6[0][0] \\
mid_{10}[0][1] = mid_6[0][1] \\
mid_{10}[1][0] = mid_6[1][0] \\
mid_{10}[1][1] = mid_6[1][1]
\end{aligned}
\end{equation}

En (s11) y utilizando \ref{eq:s12} tenemos:
\begin{equation} \label{eq:s13}
\begin{aligned}
mid_{11}[0][0] = mid_{10}[0][0] = mid_6[0][0] \\
mid_{11}[0][1] = mid_{10}[0][1] = mid_6[0][1] \\
mid_{11}[1][0] = mid_{10}[1][1] = mid_6[1][1] \\
mid_{11}[1][1] = mid_{10}[1][0] = mid_6[1][0]
\end{aligned}
\end{equation}

En (s6):
\begin{equation} \label{eq:s14}
\begin{aligned}
mid_6[0][0] = mid_5[0][0] \\
mid_6[0][1] = mid_5[0][1] \\
mid_6[1][0] = mid_5[1][1] \\
mid_6[1][1] = mid_5[1][0]
\end{aligned}
\end{equation}

Sustituimos \ref{eq:s14} en \ref{eq:s13} y nos queda:
\begin{equation} \label{eq:s15}
\begin{aligned}
mid_{11}[0][0] = mid_5[0][0] \\
mid_{11}[0][1] = mid_5[0][1] \\
mid_{11}[1][0] = mid_5[1][0] \\
mid_{11}[1][1] = mid_5[1][1]
\end{aligned}
\end{equation}

Por (s12) sabemos:
\begin{equation} \label{eq:s17}
\begin{aligned}
mid_{12}[0][0] = mid_{11}[0][0] \oplus kid1[0][0] \\
mid_{12}[0][1] = mid_{11}[0][1] \oplus kid1[0][1] \\
mid_{12}[1][0] = mid_{11}[1][0] \oplus kid1[1][0] \\
mid_{12}[1][1] = mid_{11}[1][1] \oplus kid1[1][1]
\end{aligned}
\end{equation}

Sustituimos (\ref{eq:s15}) en (\ref{eq:s17}) y obtenemos:
\begin{equation} \label{eq:s18}
\begin{aligned}
mid_{12}[0][0] = mid_5[0][0] \oplus kid1[0][0] \\
mid_{12}[0][1] = mid_5[0][1] \oplus kid1[0][1] \\
mid_{12}[1][0] = mid_5[1][0] \oplus kid1[1][0] \\
mid_{12}[1][1] = mid_5[1][1] \oplus kid1[1][1]
\end{aligned}
\end{equation}

Luego sustituimos (s5) en (\ref{eq:s18}):
\begin{equation} \label{eq:s16}
\begin{aligned}
mid_{12}[0][0] &= mid_4[0][0] \oplus kid1[0][0] \oplus kid1[0][0] \\
               &= mid_4[0][0] \\
mid_{12}[0][1] &= mid_4[0][1] \oplus kid1[0][1] \oplus kid1[0][1] \\
               &= mid_4[0][1] \\
mid_{12}[1][0] &= mid_4[1][0] \oplus kid1[1][0] \oplus kid1[1][0] \\
               &= mid_4[1][0] \\
mid_{12}[1][1] &= mid_4[1][1] \oplus kid1[1][1] \oplus kid1[1][1] \\
               &= mid_4[1][1]
\end{aligned}
\end{equation}

En (s13) y utilizando (\ref{eq:s16}) tenemos:
\begin{equation} \label{eq:s19}
\begin{aligned}
mid_{13}[0][0] = mult\_table[mid_4[0][0]][mid_4[1][0]] \\
mid_{13}[0][1] = mult\_table[mid_4[0][1]][mid_4[1][1]] \\
mid_{13}[1][0] = mult\_table[mid_4[1][0]][mid_4[0][0]] \\
mid_{13}[1][1] = mult\_table[mid_4[1][1]][mid_4[0][1]]
\end{aligned}
\end{equation}

Por (s4) sabemos que:
\begin{equation} \label{eq:s20}
\begin{aligned}
mid_4[0][0] = mult\_table[mid_3[0][0]][mid_3[1][0]] \\
mid_4[0][1] = mult\_table[mid_3[0][1]][mid_3[1][1]] \\
mid_4[1][0] = mult\_table[mid_3[1][0]][mid_3[0][0]] \\
mid_4[1][1] = mult\_table[mid_3[1][1]][mid_3[0][1]]
\end{aligned}
\end{equation}

Sustituimos (\ref{eq:s20}) en (\ref{eq:s19}) y nos queda lo siguiente:
\begin{equation} \label{eq:s21}
\begin{aligned}
mid_{13}[0][0] &= mult\_table[mult\_table[mid_3[0][0]][mid_3[1][0]]][mult\_table[mid_3[1][0]][mid_3[0][0]]] \\
               &= mid_3[0][0] \\
mid_{13}[0][1] &= mult\_table[mult\_table[mid_3[0][1]][mid_3[1][1]]][mult\_table[mid_3[1][1]][mid_3[0][1]]] \\
               &= mid_3[0][1] \\
mid_{13}[1][0] &= mult\_table[mult\_table[mid_3[1][0]][mid_3[0][0]]][mult\_table[mid_3[0][0]][mid_3[1][0]]] \\
               &= mid_3[1][0] \\
mid_{13}[1][1] &= mult\_table[mult\_table[mid_3[1][1]][mid_3[0][1]]][mult\_table[mid_3[0][1]][mid_3[1][1]]] \\
               &= mid_3[1][1]
\end{aligned}
\end{equation}
Las segundas igualdades se derivan del lema mult\_table\_inv.

En (s14) y utilizando \ref{eq:s21} tenemos:
\begin{equation} \label{eq:s22}
\begin{aligned}
mid_{14}[0][0] = mid_{13}[0][0] = mid_3[0][0] \\
mid_{14}[0][1] = mid_{13}[0][1] = mid_3[0][1] \\
mid_{14}[1][0] = mid_{13}[1][1] = mid_3[1][1] \\
mid_{14}[1][1] = mid_{13}[1][0] = mid_3[1][0]
\end{aligned}
\end{equation}

En (s3):
\begin{equation} \label{eq:s23}
\begin{aligned}
mid_3[0][0] = mid_2[0][0] \\
mid_3[0][1] = mid_2[0][1] \\
mid_3[1][0] = mid_2[1][1] \\
mid_3[1][1] = mid_2[1][0]
\end{aligned}
\end{equation}

Sustituimos \ref{eq:s23} en \ref{eq:s22} y nos queda:
\begin{equation} \label{eq:s24}
\begin{aligned}
mid_{14}[0][0] = mid_2[0][0] \\
mid_{14}[0][1] = mid_2[0][1] \\
mid_{14}[1][0] = mid_2[1][0] \\
mid_{14}[1][1] = mid_2[1][1]
\end{aligned}
\end{equation}

En (s15) sustituyendo con lo obtenido en (\ref{eq:s24}) tenemos:
\begin{equation} \label{eq:s25}
\begin{aligned}
mid_15[0][0] = sboxInv[mid_2[0][0]] \\
mid_15[0][1] = sboxInv[mid_2[0][1]] \\
mid_15[1][0] = sboxInv[mid_2[1][0]] \\
mid_15[1][1] = sboxInv[mid_2[1][1]]
\end{aligned}
\end{equation}

Sustituyendo en (\ref{eq:s25}) con las equaciones de (s2) nos queda
\begin{equation} \label{eq:s26}
\begin{aligned}
mid_15[0][0] &= sboxInv[sbox[mid_1[0][0]]] \\
             &= mid_1[0][0] \\
mid_15[0][1] &= sboxInv[sbox[mid_1[0][1]]] \\
             &= mid_1[0][1] \\
mid_15[1][0] &= sboxInv[sbox[mid_1[1][0]]] \\
             &= mid_1[1][0] \\
mid_15[1][1] &= sboxInv[sbox[mid_1[1][1]]] \\
             &= mid_1[1][1]
\end{aligned}
\end{equation}

Ahora sustituyendo (\ref{eq:s26}) en (s16):
\begin{equation} \label{eq:s27}
\begin{aligned}
mid_{16}[0][0] = mid_1[0][0] \oplus kid2[0][0] \\
mid_{16}[0][1] = mid_1[0][1] \oplus kid2[0][1] \\
mid_{16}[1][0] = mid_1[1][0] \oplus kid2[1][0] \\
mid_{16}[1][1] = mid_1[1][1] \oplus kid2[1][1]
\end{aligned}
\end{equation}

Finalmente sustituimos (s1) en (\ref{eq:s27}) y llegamos a:
\begin{equation*}
\begin{aligned}
mid_{16}[0][0] &= mid_0[0][0] \oplus kid2[0][0] \oplus kid2[0][0] \\
               &= mid_0[0][0] \\
mid_{16}[0][1] &= mid_0[0][1] \oplus kid2[0][1] \oplus kid2[0][1] \\
               &= mid_0[0][1] \\
mid_{16}[1][0] &= mid_0[1][0] \oplus kid2[1][0] \oplus kid2[1][0] \\
               &= mid_0[1][0] \\
mid_{16}[1][1] &= mid_0[1][1] \oplus kid2[1][1] \oplus kid2[1][1] \\
               &= mid_0[1][1]
\end{aligned}
\end{equation*}


\end{document}
